|
dlinear
0.0.1
Delta-complete SMT solver for linear programming
|
|
|
dlinear
0.0.1
Delta-complete SMT solver for linear programming
|
| ▼Ndlinear | Global namespace for the dlinear library |
| ▼Ndrake | |
| ►Nsymbolic | |
| 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::Variables > | Computes the hash value of a symbolic variables |
| ▼Nmps | Namespace for the MPS parser of the dlinear library |
| CMpsDriver | Brings together all components |
| CMpsScanner | MpsScanner is a derived class to add some extra function to the scanner class |
| ▼Nonnx | Namespace for the ONNX parser of the dlinear library |
| COnnxDriver | Reads the onnx file |
| CTensor | |
| ▼Nqsopt_ex | |
| CMpqArray | A wrapper around an array of mpq_t elements |
| ▼Nsmt2 | Namespace for the SMT2 parser of the dlinear library |
| CFunctionDefinition | A new function defined by the user in the SMT2 language using the define-fun command |
| CSmt2Driver | Brings together all components |
| CSmt2Scanner | Smt2Scanner is a derived class to add some extra function to the scanner class |
| CTerm | Generic term that can be either an expression or a formula |
| ▼Nvnnlib | Namespace for the VNNLIB parser of the dlinear library |
| CFunctionDefinition | A new function defined by the user in the VNNLIB language using the define-fun command |
| CTerm | Generic term that can be either an expression or a formula |
| CVnnlibDriver | Brings together all components |
| CVnnlibScanner | VnnlibScanner is a derived class to add some extra function to the scanner class |
| CArgParser | Used to parse command line arguments and produce a corresponding Config object to be used throughout the execution |
| CBitIncrementIterator | BitIncrementIterator class |
| CBound | Tuple containing the value, bound type and theory literal associated with the bound |
| ▼CBoundImplicator | Use theory reasoning to add relations between literals using some simple theory inferences |
| CConstraint | Constraint |
| CBoundIterator | BoundIterator class |
| CBoundPreprocessor | This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver |
| CBoundVector | Data structure to store the LP solver bounds in a sorted vector to determine the active lower and upper bound for the column |
| CBox | Collection of variables with associated intervals |
| CCadicalSatSolver | SAT solver based on CaDiCal |
| ▼CCompleteSoplexTheorySolver | Complete solver using SoPlex |
| CNqExplanation | Structure used to store the infeasibility explanation of a subset of non-equal constraints |
| CConfig | Simple dataclass used to store the configuration of the program |
| ▼CContext | Context class that holds the set of constraints and provide Assert/Push/Pop/CheckSat functionalities |
| CImpl | The context juggles between the SAT solver and the theory solver, in order to produce a model |
| CDeltaQsoptexTheorySolver | Delta complete solver using QSopt_ex |
| CDeltaSoplexTheorySolver | Delta complete solver using SoPlex |
| CDriver | The Driver is the base class for all the parsers |
| CEdgeEqual_ | |
| CExpressionEvaluator | Evaluate an expression with a given box |
| CFormulaVisitor | This base class provides all the methods expected to visit the underlying formula and return a modified version |
| CGenericExpressionVisitor | Generic expression visitor implementing the visitor pattern |
| CGenericFormulaVisitor | Generic formula visitor implementing the visitor pattern |
| CGraph | Graph class |
| CIfThenElseEliminator | IfThenElseEliminator class |
| CInfinity | Global class storing the infinity values for the different LP solvers |
| CInterval | |
| CIterationStats | Dataclass collecting statistics about some operation or process |
| CLeakyReluConstraint | |
| CLinearFormulaFlattener | Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard form |
| CLiteral | A literal is a variable with an associated truth value, indicating whether it is true or false |
| CNaiveCnfizer | Transforms a symbolic formula f into a CNF formula by preserving its semantics |
| CNnfizer | Implementation of NNF (Negation Normal Form) conversion |
| ▼CNNSoplexTheorySolver | Specialised theory solver for neural networks using SoPlex |
| CPlConstraint | |
| CNumericDataContainer | NumericDataContainer class |
| COptionValue | Represents an optional value in dLinear |
| CPicosatSatSolver | PicoSAT is a SAT solver written in C |
| CPiecewiseLinearConstraint | A piecewise linear constraint is a constraint that assumes different linear functions depending on the truth assignment of a literal |
| CPlaistedGreenbaumCnfizer | Plaisted-Greenbaum transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF |
| CPredicateAbstractor | Predicate abstraction is a method to convert a first-order logic formula into a Boolean formula |
| CPrefixPrinter | Print expressions and formulas in prefix-form |
| CQsoptexTheorySolver | QSopt_ex is an exact LP solver written in C |
| CReluConstraint | A ReLU constraint is a kind of piecewise linear constraint |
| CRoundingModeGuard | |
| CSatSolver | Base class for SAT solvers |
| CScopedUnorderedMap | |
| CScopedUnorderedSet | |
| CScopedVector | |
| CSmtSolver | This class provides an easy interface for using the underling solver |
| CSmtSolverOutput | Data struct containing the output of the solver, such as the result of the computation as well as some statistics |
| CSoplexTheorySolver | SoPlex is an exact LP solver written in C++ |
| CSortedVector | Vector that maintains its elements sorted |
| CStats | Dataclass collecting statistics about some operation or process |
| CTheorySolver | Base class for theory solvers |
| CTimer | Timer class using the a steady clock |
| CTimerBase | Simple timer class to evaluate the performance of the software |
| CTimerGuard | The TimeGuard wraps a timer object and pauses it when the guard object is destructed |
| CTseitinCnfizer | Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF |
| Cuser_clock | |
| CUserTimer | Timer class using the user_clock |
| ▼Nstd | STL namespace |
| Cequal_to< dlinear::drake::symbolic::Expression > | |
| Cequal_to< dlinear::drake::symbolic::Formula > | |
| Cequal_to< dlinear::drake::symbolic::Variable > | |
| Chash< dlinear::drake::symbolic::Expression > | |
| Chash< dlinear::drake::symbolic::Formula > | |
| Chash< dlinear::drake::symbolic::Variable > | |
| Chash< mpq_class > | |
| Cless< dlinear::drake::symbolic::Expression > | |
| Cless< dlinear::drake::symbolic::Formula > | |
| Cless< dlinear::drake::symbolic::Variable > | |
| Cnumeric_limits< dlinear::drake::symbolic::Expression > |
1.11.0