| CBox | Represents a n-dimensional interval vector |
| CCachedExpression | Cached expression class |
| CCdsInit | |
| CCdsScopeGuard | |
| CCommand | Command class in smt2lib |
| ►CCommandCell | CommandCell class |
| CAssertCommand | "assert" command |
| CCheckSatCommand | "check-sat" command |
| CEchoCommand | "echo" command |
| CExitCommand | "exit" command |
| 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 |
| CPopCommand | "pop" command |
| CPushCommand | "push" command |
| CResetAssertionsCommand | "reset-assertions" command |
| CResetCommand | "reset" command |
| CSetInfoCommand | "set-info" command |
| CSetLogicCommand | |
| CSetOptionCommand | |
| CConfig | |
| CContext | Context class that holds a set of constraints and provide Assert/Push/Pop/CheckSat functionalities |
| 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< ContextType > | Contractor for forall constraints |
| CContractorForallMt< ContextType > | |
| 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ₙ |
| CContractorWorklistFixpoint | Fixpoint contractor using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition |
| CContractorStatus | Contractor status |
| CCounterexampleRefiner | Refines a counterexample using local optimizations |
| CDrDriver | Brings together all components |
| ►CDrFlexLexer | |
| CDrScanner | DrScanner is a derived class to add some extra function to the scanner class |
| CEnvironment | Represents a symbolic environment (mapping from a variable to a value) |
| Cequal_to< dreal::drake::symbolic::Expression > | |
| Cequal_to< dreal::drake::symbolic::Formula > | |
| Cequal_to< dreal::drake::symbolic::Variable > | |
| CExprCtrDeleter | |
| CExpression | Represents a symbolic form of an expression |
| CExpressionAddFactory | Factory class to help build ExpressionAdd expressions |
| ►CExpressionCell | Represents an abstract class which is the base of concrete symbolic-expression classes |
| ►CBinaryExpressionCell | Represents the base class for binary expressions |
| CExpressionAtan2 | Symbolic expression representing atan2 function (arctangent function with two arguments) |
| CExpressionDiv | Symbolic expression representing division |
| CExpressionMax | Symbolic expression representing max function |
| CExpressionMin | Symbolic expression representing min function |
| CExpressionPow | Symbolic expression representing power function |
| CExpressionAdd | Symbolic expression representing an addition which is a sum of products |
| CExpressionConstant | Symbolic expression representing a floating-point constant (double) |
| CExpressionIfThenElse | Symbolic expression representing if-then-else expression |
| CExpressionMul | Symbolic expression representing a multiplication of powers |
| CExpressionNaN | Symbolic expression representing NaN (not-a-number) |
| CExpressionRealConstant | Symbolic expression representing a real constant represented by a double interval [lb, ub] |
| CExpressionUninterpretedFunction | Symbolic expression representing an uninterpreted function |
| CExpressionVar | Symbolic expression representing a variable |
| ►CUnaryExpressionCell | Represents the base class for unary expressions |
| CExpressionAbs | Symbolic expression representing absolute value function |
| CExpressionAcos | Symbolic expression representing arccosine function |
| CExpressionAsin | Symbolic expression representing arcsine function |
| CExpressionAtan | Symbolic expression representing arctangent function |
| CExpressionCos | Symbolic expression representing cosine function |
| CExpressionCosh | Symbolic expression representing hyperbolic cosine function |
| CExpressionExp | Symbolic expression representing exponentiation using the base of natural logarithms |
| CExpressionLog | Symbolic expression representing logarithms |
| 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 |
| CExpressionEvaluator | |
| CExpressionMulFactory | Factory class to help build ExpressionMul expressions |
| CFormula | Represents a symbolic form of a first-order logic formula |
| ►CFormulaCell | Represents an abstract class which is the base of concrete symbolic-formula classes (i.e |
| CFormulaFalse | Symbolic formula representing false |
| CFormulaForall | Symbolic formula representing universal quantifications (∀ x₁, ..., * xn |
| CFormulaNot | Symbolic formula representing negations (¬f) |
| CFormulaTrue | Symbolic formula representing true |
| CFormulaVar | Symbolic formula representing a Boolean variable |
| ►CNaryFormulaCell | Represents the base class for N-ary logic operators (∧ and ∨) |
| CFormulaAnd | Symbolic formula representing conjunctions (f1 ∧ .. |
| CFormulaOr | Symbolic formula representing disjunctions (f1 ∨ .. |
| ►CRelationalFormulaCell | Represents the base class for relational operators (==, !=, <, <=, >, >=) |
| CFormulaEq | Symbolic formula representing equality (e1 = e2) |
| 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) |
| 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 |
| CForallFormulaEvaluator | Evaluator for forall formulas |
| CRelationalFormulaEvaluator | Evaluator for relational formulas |
| CFunctionDefinition | |
| CGenericContractorGenerator | Converts an arbitrary formula into a contractor |
| Chash< dreal::drake::symbolic::Expression > | |
| Chash< dreal::drake::symbolic::Formula > | |
| Chash< dreal::drake::symbolic::Variable > | |
| Chash_value< T > | 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 |
| 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 |
| CIfThenElseEliminator | Eliminates If-Then-Else expressions by introducing new variables |
| CContext::Impl | |
| Cless< dreal::drake::symbolic::Expression > | |
| Cless< dreal::drake::symbolic::Formula > | |
| Cless< dreal::drake::symbolic::Variable > | |
| CMainProgram | DReal's main program |
| CNaiveCnfizer | Transforms a symbolic formula f into a CNF formula by preserving its semantics |
| Cnever_destroyed< T > | 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 |
| CNloptOptimizer | Wrapper class for nlopt |
| CNnfizer | A class implementing NNF (Negation Normal Form) conversion |
| COptionValue< T > | Represents an optional value in dReal |
| COptionValue< bool > | |
| COptionValue< Brancher > | |
| COptionValue< double > | |
| COptionValue< int > | |
| COptionValue< SatDefaultPhase > | |
| COptionValue< uint32_t > | |
| 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 | |
| CRoundingModeGuard | |
| CSatSolver | |
| CScopedUnorderedMap< Key, T, Hash, KeyEqual, Allocator > | Backtrackable map |
| CScopedUnorderedMap< int, dreal::drake::symbolic::Variable > | |
| CScopedUnorderedMap< std::string, dreal::drake::symbolic::Variable > | |
| CScopedUnorderedMap< std::string, dreal::FunctionDefinition > | |
| CScopedUnorderedMap< Variable::Id, int > | |
| CScopedUnorderedSet< Key, Hash, KeyEqual, Allocator > | Backtrackable set |
| CScopedUnorderedSet< Variable::Id > | |
| CScopedVector< T > | |
| CScopedVector< dreal::Box > | |
| CScopedVector< dreal::drake::symbolic::Formula > | |
| CSignalHandlerGuard | Sets a new signal handler and restores the old one when it goes out of scope |
| CSmt2Driver | Brings together all components |
| ►CSmt2FlexLexer | |
| CSmt2Scanner | Smt2Scanner is a derived class to add some extra function to the scanner class |
| ►CStat | Base class for statistics |
| CIcpStat | A class to show statistics information at destruction |
| 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) |
| CVariable | Represents a symbolic variable |
| CVariables | Represents a set of variables |
| ►Cnumeric_limits | |
| Cnumeric_limits< dreal::drake::symbolic::Expression > | |
1.8.13