dReal4
Class List
Here are the classes, structs, unions and interfaces with brief descriptions:
[detail level 1234]
 NdrealSum type of symbolic::Expression and symbolic::Formula
 Ndrake
 CAssertCommand"assert" command
 CBoxRepresents a n-dimensional interval vector
 CCachedExpressionCached expression class
 CCdsInit
 CCdsScopeGuard
 CCheckSatCommand"check-sat" command
 CCommandCommand class in smt2lib
 CCommandCellCommandCell class
 CConfig
 CContextContext class that holds a set of constraints and provide Assert/Push/Pop/CheckSat functionalities
 CContractor
 CContractorCellAbstract base class of contractors
 CContractorFixpointFixpoint contractor: apply C₁, ..., Cₙ until it reaches a fixpoint (technically, until it satisfies a given termination condition)
 CContractorForallContractor for forall constraints
 CContractorForallMt
 CContractorIbexFwdbwdContractor class wrapping IBEX's forward/backward contractor
 CContractorIbexFwdbwdMtMulti-thread version of ContractorIbexFwdbwd contractor
 CContractorIbexPolytope
 CContractorIbexPolytopeMtMulti-thread version of ContractorIbexFwdbwd contractor
 CContractorId
 CContractorInteger
 CContractorJoinJoin contractor
 CContractorSeqSequential contractor: Sequentially apply C₁, ..., Cₙ
 CContractorStatusContractor status
 CContractorWorklistFixpointFixpoint contractor using the worklist algorithm: apply C₁, ..., Cₙ until it reaches a fixpoint or it satisfies a given termination condition
 CCounterexampleRefinerRefines a counterexample using local optimizations
 CDrDriverBrings together all components
 CDrScannerDrScanner is a derived class to add some extra function to the scanner class
 CEchoCommand"echo" command
 CExitCommand"exit" command
 CExprCtrDeleter
 CExpressionEvaluator
 CForallFormulaEvaluatorEvaluator for forall formulas
 CFormulaEvaluationResultRepresents the evaluation result of a constraint given a box
 CFormulaEvaluatorClass to evaluate a symbolic formula with a box
 CFormulaEvaluatorCellBase type for evaluator cell types
 CFunctionDefinition
 CGenericContractorGeneratorConverts 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
 CIbexConverterVisitor class which converts a symbolic Formula into ibex::ExprCtr
 CIcpAbstract Class for ICP (Interval Constraint Propagation) algorithm
 CIcpParallelClass for Parallel ICP (Interval Constraint Propagation) algorithm
 CIcpSeqClass for ICP (Interval Constraint Propagation) algorithm
 CIcpStatA class to show statistics information at destruction
 CIfThenElseEliminatorEliminates If-Then-Else expressions by introducing new variables
 CMainProgramDReal's main program
 CNaiveCnfizerTransforms a symbolic formula f into a CNF formula by preserving its semantics
 CNloptOptimizerWrapper class for nlopt
 CNnfizerA class implementing NNF (Negation Normal Form) conversion
 COptionValueRepresents an optional value in dReal
 CPopCommand"pop" command
 CPrecisionGuardSets the decimal precision to be used to format floating-point values on output operations
 CPredicateAbstractor
 CPrefixPrinterClass to print expressions and formulas in prefix-form
 CProfiler
 CPushCommand"push" command
 CRelationalFormulaEvaluatorEvaluator for relational formulas
 CResetAssertionsCommand"reset-assertions" command
 CResetCommand"reset" command
 CRoundingModeGuard
 CSatSolver
 CScopedUnorderedMapBacktrackable map
 CScopedUnorderedSetBacktrackable set
 CScopedVector
 CSetInfoCommand"set-info" command
 CSetLogicCommand
 CSetOptionCommand
 CSignalHandlerGuardSets a new signal handler and restores the old one when it goes out of scope
 CSmt2DriverBrings together all components
 CSmt2ScannerSmt2Scanner is a derived class to add some extra function to the scanner class
 CStatBase class for statistics
 CTerm
 CTheorySolverTheory solver for nonlinear theory over the Reals
 CTimerSimple timer class to profile performance
 CTimerGuardPauses the passed timer object when the guard object is destructed (e.g
 CTseitinCnfizerTransforms a symbolic formula f into an equi-satisfiable CNF formula by introducing extra Boolean variables (Tseitin transformation)
 NstdSTL 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 >