Namespace List

Here is a list of all documented namespaces with brief descriptions:

[detail level 123]

▼Ndlinear	Global namespace for the dlinear library
▼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
RIsAnyOf	Check if the type T is any of the types U
RIsNotAnyOf	Check if the type T is not any of the types U
RArithmetic	Check if the type T supports the arithmetic operations +, -, *, /
RNumeric	Check if the type T supports the arithmetic operations +, -, *, / and the comparison operators <, >, <=, >=
▼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 >
Nxt