| Cdlinear::ArgParser | Used to parse command line arguments and produce a corresponding Config object to be used throughout the execution |
| Cdlinear::BitIncrementIterator | BitIncrementIterator class |
| Cdlinear::Bound | Tuple containing the value, bound type and theory literal associated with the bound |
| Cdlinear::BoundImplicator | Use theory reasoning to add relations between literals using some simple theory inferences |
| Cdlinear::BoundIterator | BoundIterator class |
| Cdlinear::BoundPreprocessor | This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver |
| Cdlinear::BoundVector | Data structure to store the LP solver bounds in a sorted vector to determine the active lower and upper bound for the column |
| Cdlinear::Box | Collection of variables with associated intervals |
| Cdlinear::Config | Simple dataclass used to store the configuration of the program |
| Cdlinear::BoundImplicator::Constraint | Constraint |
| Cdlinear::Context | Context class that holds the set of constraints and provide Assert/Push/Pop/CheckSat functionalities |
| ►Cdlinear::Driver | The Driver is the base class for all the parsers |
| Cdlinear::mps::MpsDriver | Brings together all components |
| Cdlinear::onnx::OnnxDriver | Reads the onnx file |
| Cdlinear::smt2::Smt2Driver | Brings together all components |
| Cdlinear::vnnlib::VnnlibDriver | Brings together all components |
| Cdlinear::EdgeEqual_< T, W > | |
| Cdlinear::drake::symbolic::Environment | Represents a symbolic environment (mapping from a variable to a value) |
| Cstd::equal_to< dlinear::drake::symbolic::Expression > | |
| Cstd::equal_to< dlinear::drake::symbolic::Formula > | |
| Cstd::equal_to< dlinear::drake::symbolic::Variable > | |
| Cdlinear::drake::symbolic::Expression | Represents a symbolic form of an expression |
| Cdlinear::drake::symbolic::ExpressionAddFactory | Factory class to help build ExpressionAdd expressions |
| ►Cdlinear::drake::symbolic::ExpressionCell | Represents an abstract class which is the base of concrete symbolic-expression classes |
| ►Cdlinear::drake::symbolic::BinaryExpressionCell | Represents the base class for binary expressions |
| Cdlinear::drake::symbolic::ExpressionAtan2 | Symbolic expression representing atan2 function (arctangent function with two arguments) |
| Cdlinear::drake::symbolic::ExpressionDiv | Symbolic expression representing division |
| Cdlinear::drake::symbolic::ExpressionMax | Symbolic expression representing max function |
| Cdlinear::drake::symbolic::ExpressionMin | Symbolic expression representing min function |
| Cdlinear::drake::symbolic::ExpressionPow | Symbolic expression representing power function |
| Cdlinear::drake::symbolic::ExpressionAdd | Symbolic expression representing an addition which is a sum of products |
| Cdlinear::drake::symbolic::ExpressionConstant | Symbolic expression representing a rational constant (mpq_class) |
| Cdlinear::drake::symbolic::ExpressionIfThenElse | Symbolic expression representing if-then-else expression |
| Cdlinear::drake::symbolic::ExpressionInfty | Symbolic expression representing infinities |
| Cdlinear::drake::symbolic::ExpressionMul | Symbolic expression representing a multiplication of powers |
| Cdlinear::drake::symbolic::ExpressionNaN | Symbolic expression representing NaN (not-a-number) |
| Cdlinear::drake::symbolic::ExpressionUninterpretedFunction | Symbolic expression representing an uninterpreted function |
| Cdlinear::drake::symbolic::ExpressionVar | Symbolic expression representing a variable |
| ►Cdlinear::drake::symbolic::UnaryExpressionCell | Represents the base class for unary expressions |
| Cdlinear::drake::symbolic::ExpressionAbs | Symbolic expression representing absolute value function |
| Cdlinear::drake::symbolic::ExpressionAcos | Symbolic expression representing arccosine function |
| Cdlinear::drake::symbolic::ExpressionAsin | Symbolic expression representing arcsine function |
| Cdlinear::drake::symbolic::ExpressionAtan | Symbolic expression representing arctangent function |
| Cdlinear::drake::symbolic::ExpressionCos | Symbolic expression representing cosine function |
| Cdlinear::drake::symbolic::ExpressionCosh | Symbolic expression representing hyperbolic cosine function |
| Cdlinear::drake::symbolic::ExpressionExp | Symbolic expression representing exponentiation using the base of natural logarithms |
| Cdlinear::drake::symbolic::ExpressionLog | Symbolic expression representing logarithms |
| Cdlinear::drake::symbolic::ExpressionSin | Symbolic expression representing sine function |
| Cdlinear::drake::symbolic::ExpressionSinh | Symbolic expression representing hyperbolic sine function |
| Cdlinear::drake::symbolic::ExpressionSqrt | Symbolic expression representing square-root |
| Cdlinear::drake::symbolic::ExpressionTan | Symbolic expression representing tangent function |
| Cdlinear::drake::symbolic::ExpressionTanh | Symbolic expression representing hyperbolic tangent function |
| Cdlinear::drake::symbolic::ExpressionMulFactory | Factory class to help build ExpressionMul expressions |
| Cdlinear::drake::symbolic::Formula | Represents a symbolic form of a first-order logic formula |
| Cdlinear::smt2::FunctionDefinition | A new function defined by the user in the SMT2 language using the define-fun command |
| Cdlinear::vnnlib::FunctionDefinition | A new function defined by the user in the VNNLIB language using the define-fun command |
| Cdlinear::GenericExpressionVisitor< Result, Args > | Generic expression visitor implementing the visitor pattern |
| ►Cdlinear::GenericExpressionVisitor< Expression, const Formula & > | |
| Cdlinear::IfThenElseEliminator | IfThenElseEliminator class |
| ►Cdlinear::GenericExpressionVisitor< Interval, const Box & > | |
| Cdlinear::ExpressionEvaluator | Evaluate an expression with a given box |
| ►Cdlinear::GenericExpressionVisitor< std::ostream & > | |
| Cdlinear::PrefixPrinter | Print expressions and formulas in prefix-form |
| Cdlinear::GenericFormulaVisitor< Result, Args > | Generic formula visitor implementing the visitor pattern |
| ►Cdlinear::GenericFormulaVisitor< Formula, Args... > | |
| ►Cdlinear::FormulaVisitor< const Formula & > | |
| Cdlinear::IfThenElseEliminator | IfThenElseEliminator class |
| ►Cdlinear::FormulaVisitor<> | |
| Cdlinear::NaiveCnfizer | Transforms a symbolic formula f into a CNF formula by preserving its semantics |
| Cdlinear::PredicateAbstractor | Predicate abstraction is a method to convert a first-order logic formula into a Boolean formula |
| ►Cdlinear::FormulaVisitor< bool, bool > | |
| Cdlinear::Nnfizer | Implementation of NNF (Negation Normal Form) conversion |
| ►Cdlinear::FormulaVisitor< std::vector< Formula > &, std::vector< Variable > & > | |
| Cdlinear::PlaistedGreenbaumCnfizer | Plaisted-Greenbaum transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF |
| ►Cdlinear::FormulaVisitor< std::map< Variable, Formula > & > | |
| Cdlinear::TseitinCnfizer | Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF |
| Cdlinear::FormulaVisitor< Args > | This base class provides all the methods expected to visit the underlying formula and return a modified version |
| ►Cdlinear::GenericFormulaVisitor< std::ostream & > | |
| Cdlinear::PrefixPrinter | Print expressions and formulas in prefix-form |
| Cdlinear::Graph< T, W, EdgeHash, EdgeEqual > | Graph class |
| Cstd::hash< dlinear::drake::symbolic::Expression > | |
| Cstd::hash< dlinear::drake::symbolic::Formula > | |
| Cstd::hash< dlinear::drake::symbolic::Variable > | |
| Cstd::hash< mpq_class > | |
| Cdlinear::drake::hash_value< T > | Computes the hash value of v using std::hash |
| Cdlinear::drake::hash_value< std::map< T1, T2 > > | Computes the hash value of a map map |
| Cdlinear::drake::hash_value< std::pair< T1, T2 > > | Computes the hash value of a pair p |
| Cdlinear::drake::hash_value< std::set< T > > | Computes the hash value of a set s |
| Cdlinear::drake::hash_value< std::vector< T > > | Computes the hash value of a vector vec |
| Cdlinear::drake::hash_value< symbolic::Variables > | Computes the hash value of a symbolic variables |
| Cdlinear::Context::Impl | The context juggles between the SAT solver and the theory solver, in order to produce a model |
| Cdlinear::Infinity | Global class storing the infinity values for the different LP solvers |
| Cdlinear::Interval | |
| Cstd::less< dlinear::drake::symbolic::Expression > | |
| Cstd::less< dlinear::drake::symbolic::Formula > | |
| Cstd::less< dlinear::drake::symbolic::Variable > | |
| Cdlinear::LinearFormulaFlattener | Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard form |
| Cdlinear::Literal | A literal is a variable with an associated truth value, indicating whether it is true or false |
| Cdlinear::qsopt_ex::MpqArray | A wrapper around an array of mpq_t elements |
| ►CMpsFlexLexer | |
| Cdlinear::mps::MpsScanner | MpsScanner is a derived class to add some extra function to the scanner class |
| Cdlinear::CompleteSoplexTheorySolver::NqExplanation | Structure used to store the infeasibility explanation of a subset of non-equal constraints |
| ►Cnumeric_limits | |
| Cstd::numeric_limits< dlinear::drake::symbolic::Expression > | |
| Cdlinear::NumericDataContainer< N, D > | NumericDataContainer class |
| Cdlinear::OptionValue< T > | Represents an optional value in dLinear |
| Cdlinear::OptionValue< bool > | |
| Cdlinear::OptionValue< BoundPropagationType > | |
| Cdlinear::OptionValue< double > | |
| Cdlinear::OptionValue< Format > | |
| Cdlinear::OptionValue< int > | |
| Cdlinear::OptionValue< LPMode > | |
| Cdlinear::OptionValue< LPSolver > | |
| Cdlinear::OptionValue< PreprocessingRunningFrequency > | |
| Cdlinear::OptionValue< SatDefaultPhase > | |
| Cdlinear::OptionValue< SatSolver > | |
| Cdlinear::OptionValue< std::string > | |
| Cdlinear::OptionValue< unsigned int > | |
| ►Cdlinear::PiecewiseLinearConstraint | A piecewise linear constraint is a constraint that assumes different linear functions depending on the truth assignment of a literal |
| Cdlinear::LeakyReluConstraint | |
| Cdlinear::ReluConstraint | A ReLU constraint is a kind of piecewise linear constraint |
| Cdlinear::NNSoplexTheorySolver::PlConstraint | |
| Cdlinear::RoundingModeGuard | |
| ►Cdlinear::SatSolver | Base class for SAT solvers |
| Cdlinear::CadicalSatSolver | SAT solver based on CaDiCal |
| Cdlinear::PicosatSatSolver | PicoSAT is a SAT solver written in C |
| Cdlinear::ScopedUnorderedMap< Key, T, Hash, KeyEqual, Allocator > | |
| Cdlinear::ScopedUnorderedMap< int, dlinear::drake::symbolic::Variable > | |
| Cdlinear::ScopedUnorderedMap< std::string, dlinear::drake::symbolic::Expression > | |
| Cdlinear::ScopedUnorderedMap< std::string, dlinear::drake::symbolic::Variable > | |
| Cdlinear::ScopedUnorderedMap< std::string, dlinear::smt2::FunctionDefinition > | |
| Cdlinear::ScopedUnorderedMap< std::string, dlinear::vnnlib::FunctionDefinition > | |
| Cdlinear::ScopedUnorderedMap< Variable::Id, int > | |
| Cdlinear::ScopedUnorderedSet< Key, Hash, KeyEqual, Allocator > | |
| Cdlinear::ScopedUnorderedSet< Variable::Id > | |
| Cdlinear::ScopedVector< T > | |
| Cdlinear::ScopedVector< dlinear::Box > | |
| Cdlinear::ScopedVector< dlinear::drake::symbolic::Formula > | |
| ►CSmt2FlexLexer | |
| Cdlinear::smt2::Smt2Scanner | Smt2Scanner is a derived class to add some extra function to the scanner class |
| Cdlinear::SmtSolver | This class provides an easy interface for using the underling solver |
| Cdlinear::SmtSolverOutput | Data struct containing the output of the solver, such as the result of the computation as well as some statistics |
| Cdlinear::SortedVector< T, Compare > | Vector that maintains its elements sorted |
| Cdlinear::SortedVector< Bound > | |
| Cdlinear::SortedVector< dlinear::BoundImplicator::Constraint > | |
| ►Cdlinear::Stats | Dataclass collecting statistics about some operation or process |
| Cdlinear::IterationStats | Dataclass collecting statistics about some operation or process |
| Cdlinear::onnx::Tensor | |
| Cdlinear::smt2::Term | Generic term that can be either an expression or a formula |
| Cdlinear::vnnlib::Term | Generic term that can be either an expression or a formula |
| ►Cdlinear::TheorySolver | Base class for theory solvers |
| ►Cdlinear::QsoptexTheorySolver | QSopt_ex is an exact LP solver written in C |
| Cdlinear::DeltaQsoptexTheorySolver | Delta complete solver using QSopt_ex |
| ►Cdlinear::SoplexTheorySolver | SoPlex is an exact LP solver written in C++ |
| Cdlinear::CompleteSoplexTheorySolver | Complete solver using SoPlex |
| Cdlinear::DeltaSoplexTheorySolver | Delta complete solver using SoPlex |
| Cdlinear::NNSoplexTheorySolver | Specialised theory solver for neural networks using SoPlex |
| Cdlinear::TimerBase< T > | Simple timer class to evaluate the performance of the software |
| ►Cdlinear::TimerBase< chosen_steady_clock > | |
| Cdlinear::Timer | Timer class using the a steady clock |
| ►Cdlinear::TimerBase< user_clock > | |
| Cdlinear::UserTimer | Timer class using the user_clock |
| Cdlinear::TimerGuard | The TimeGuard wraps a timer object and pauses it when the guard object is destructed |
| Cdlinear::user_clock | |
| Cdlinear::drake::symbolic::Variable | Represents a symbolic variable |
| Cdlinear::drake::symbolic::Variables | Represents a set of variables |
| ►CVnnlibFlexLexer | |
| Cdlinear::vnnlib::VnnlibScanner | VnnlibScanner is a derived class to add some extra function to the scanner class |
1.11.0