▼Ndreal | Sum type of symbolic::Expression and symbolic::Formula |
►Ndrake | |
►Nsymbolic | |
CBinaryExpressionCell | Represents the base class for binary expressions |
CEnvironment | Represents a symbolic environment (mapping from a variable to a value) |
CExpression | Represents a symbolic form of an expression |
CExpressionAbs | Symbolic expression representing absolute value function |
CExpressionAcos | Symbolic expression representing arccosine function |
CExpressionAdd | Symbolic expression representing an addition which is a sum of products |
CExpressionAddFactory | Factory class to help build ExpressionAdd expressions |
CExpressionAsin | Symbolic expression representing arcsine function |
CExpressionAtan | Symbolic expression representing arctangent function |
CExpressionAtan2 | Symbolic expression representing atan2 function (arctangent function with two arguments) |
CExpressionCell | Represents an abstract class which is the base of concrete symbolic-expression classes |
CExpressionConstant | Symbolic expression representing a floating-point constant (double) |
CExpressionCos | Symbolic expression representing cosine function |
CExpressionCosh | Symbolic expression representing hyperbolic cosine function |
CExpressionDiv | Symbolic expression representing division |
CExpressionExp | Symbolic expression representing exponentiation using the base of natural logarithms |
CExpressionIfThenElse | Symbolic expression representing if-then-else expression |
CExpressionLog | Symbolic expression representing logarithms |
CExpressionMax | Symbolic expression representing max function |
CExpressionMin | Symbolic expression representing min function |
CExpressionMul | Symbolic expression representing a multiplication of powers |
CExpressionMulFactory | Factory class to help build ExpressionMul expressions |
CExpressionNaN | Symbolic expression representing NaN (not-a-number) |
CExpressionPow | Symbolic expression representing power function |
CExpressionRealConstant | Symbolic expression representing a real constant represented by a double interval [lb, ub] |
CExpressionSin | Symbolic expression representing sine function |
CExpressionSinh | Symbolic expression representing hyperbolic sine function |
CExpressionSqrt | Symbolic expression representing square-root |
CExpressionTan | Symbolic expression representing tangent function |
CExpressionTanh | Symbolic expression representing hyperbolic tangent function |
CExpressionUninterpretedFunction | Symbolic expression representing an uninterpreted function |
CExpressionVar | Symbolic expression representing a variable |
CFormula | Represents a symbolic form of a first-order logic formula |
CFormulaAnd | Symbolic formula representing conjunctions (f1 ∧ .. |
CFormulaCell | Represents an abstract class which is the base of concrete symbolic-formula classes (i.e |
CFormulaEq | Symbolic formula representing equality (e1 = e2) |
CFormulaFalse | Symbolic formula representing false |
CFormulaForall | Symbolic formula representing universal quantifications (∀ x₁, ..., * xn |
CFormulaGeq | Symbolic formula representing 'greater-than-or-equal-to' (e1 ≥ e2) |
CFormulaGt | Symbolic formula representing 'greater-than' (e1 > e2) |
CFormulaLeq | Symbolic formula representing 'less-than-or-equal-to' (e1 ≤ e2) |
CFormulaLt | Symbolic formula representing 'less-than' (e1 < e2) |
CFormulaNeq | Symbolic formula representing disequality (e1 ≠ e2) |
CFormulaNot | Symbolic formula representing negations (¬f) |
CFormulaOr | Symbolic formula representing disjunctions (f1 ∨ .. |
CFormulaTrue | Symbolic formula representing true |
CFormulaVar | Symbolic formula representing a Boolean variable |
CNaryFormulaCell | Represents the base class for N-ary logic operators (∧ and ∨) |
CRelationalFormulaCell | Represents the base class for relational operators (==, !=, <, <=, >, >=) |
CUnaryExpressionCell | Represents the base class for unary expressions |
CVariable | Represents a symbolic variable |
CVariables | Represents a set of variables |
Chash_value | Computes the hash value of v using std::hash |
Chash_value< std::map< T1, T2 > > | Computes the hash value of a map map |
Chash_value< std::pair< T1, T2 > > | Computes the hash value of a pair p |
Chash_value< std::set< T > > | Computes the hash value of a set s |
Chash_value< std::vector< T > > | Computes the hash value of a vector vec |
Chash_value< symbolic::Expression > | Computes the hash value of a symbolic expression |
Chash_value< symbolic::Formula > | Computes the hash value of a symbolic formula |
Chash_value< symbolic::Variable > | Computes the hash value of a variable |
Chash_value< symbolic::Variables > | Computes the hash value of a symbolic variables |
Cnever_destroyed | Wraps an underlying type T such that its storage is a direct member field of this object (i.e., without any indirection into the heap), but unlike most member fields T's destructor is never invoked |
CAssertCommand | "assert" command |
CBox | Represents a n-dimensional interval vector |
CCachedExpression | Cached expression class |
CCdsInit | |
CCdsScopeGuard | |
CCheckSatCommand | "check-sat" command |
CCommand | Command class in smt2lib |
CCommandCell | CommandCell class |
CConfig | |
►CContext | Context class that holds a set of constraints and provide Assert/Push/Pop/CheckSat functionalities |
CImpl | |
CContractor | |
CContractorCell | Abstract base class of contractors |
CContractorFixpoint | Fixpoint contractor: apply C₁, ..., Cₙ until it reaches a fixpoint (technically, until it satisfies a given termination condition) |
CContractorForall | Contractor for forall constraints |
CContractorForallMt | |
CContractorIbexFwdbwd | Contractor class wrapping IBEX's forward/backward contractor |
CContractorIbexFwdbwdMt | Multi-thread version of ContractorIbexFwdbwd contractor |
CContractorIbexPolytope | |
CContractorIbexPolytopeMt | Multi-thread version of ContractorIbexFwdbwd contractor |
CContractorId | |
CContractorInteger | |
CContractorJoin | Join contractor |
CContractorSeq | Sequential contractor: Sequentially apply C₁, ..., Cₙ |
CContractorStatus | Contractor status |
CContractorWorklistFixpoint | Fixpoint contractor using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition |
CCounterexampleRefiner | Refines a counterexample using local optimizations |
CDrDriver | Brings together all components |
CDrScanner | DrScanner is a derived class to add some extra function to the scanner class |
CEchoCommand | "echo" command |
CExitCommand | "exit" command |
CExprCtrDeleter | |
CExpressionEvaluator | |
CForallFormulaEvaluator | Evaluator for forall formulas |
CFormulaEvaluationResult | Represents the evaluation result of a constraint given a box |
CFormulaEvaluator | Class to evaluate a symbolic formula with a box |
CFormulaEvaluatorCell | Base type for evaluator cell types |
CFunctionDefinition | |
CGenericContractorGenerator | Converts an arbitrary formula into a contractor |
CGetAssertionsCommand | "get-assertions" command |
CGetAssignmentCommand | "get-assignments" command |
CGetInfoCommand | "get-info" command |
CGetModelCommand | "get-model" command |
CGetOptionCommand | "get-option" command |
CGetProofCommand | "get-proof" command |
CGetUnsatAssumptionsCommand | "get-unsat-assumptions" command |
CGetUnsatCoreCommand | "get-unsat-core" command |
CIbexConverter | Visitor class which converts a symbolic Formula into ibex::ExprCtr |
CIcp | Abstract Class for ICP (Interval Constraint Propagation) algorithm |
CIcpParallel | Class for Parallel ICP (Interval Constraint Propagation) algorithm |
CIcpSeq | Class for ICP (Interval Constraint Propagation) algorithm |
CIcpStat | A class to show statistics information at destruction |
CIfThenElseEliminator | Eliminates If-Then-Else expressions by introducing new variables |
CMainProgram | DReal's main program |
CNaiveCnfizer | Transforms a symbolic formula f into a CNF formula by preserving its semantics |
CNloptOptimizer | Wrapper class for nlopt |
CNnfizer | A class implementing NNF (Negation Normal Form) conversion |
COptionValue | Represents an optional value in dReal |
CPopCommand | "pop" command |
CPrecisionGuard | Sets the decimal precision to be used to format floating-point values on output operations |
CPredicateAbstractor | |
CPrefixPrinter | Class to print expressions and formulas in prefix-form |
CProfiler | |
CPushCommand | "push" command |
CRelationalFormulaEvaluator | Evaluator for relational formulas |
CResetAssertionsCommand | "reset-assertions" command |
CResetCommand | "reset" command |
CRoundingModeGuard | |
CSatSolver | |
CScopedUnorderedMap | Backtrackable map |
CScopedUnorderedSet | Backtrackable set |
CScopedVector | |
CSetInfoCommand | "set-info" command |
CSetLogicCommand | |
CSetOptionCommand | |
CSignalHandlerGuard | Sets a new signal handler and restores the old one when it goes out of scope |
CSmt2Driver | Brings together all components |
CSmt2Scanner | Smt2Scanner is a derived class to add some extra function to the scanner class |
CStat | Base class for statistics |
CTerm | |
CTheorySolver | Theory solver for nonlinear theory over the Reals |
CTimer | Simple timer class to profile performance |
CTimerGuard | Pauses the passed timer object when the guard object is destructed (e.g |
CTseitinCnfizer | Transforms a symbolic formula f into an equi-satisfiable CNF formula by introducing extra Boolean variables (Tseitin transformation) |
▼Nstd | STL namespace |
Cequal_to< dreal::drake::symbolic::Expression > | |
Cequal_to< dreal::drake::symbolic::Formula > | |
Cequal_to< dreal::drake::symbolic::Variable > | |
Chash< dreal::drake::symbolic::Expression > | |
Chash< dreal::drake::symbolic::Formula > | |
Chash< dreal::drake::symbolic::Variable > | |
Cless< dreal::drake::symbolic::Expression > | |
Cless< dreal::drake::symbolic::Formula > | |
Cless< dreal::drake::symbolic::Variable > | |
Cnumeric_limits< dreal::drake::symbolic::Expression > | |