|
dlinear
0.0.1
Delta-complete SMT solver for linear programming
|
|
|
dlinear
0.0.1
Delta-complete SMT solver for linear programming
|
Global namespace for the dlinear library. More...
Namespaces | |
| namespace | mps |
| Namespace for the MPS parser of the dlinear library. | |
| namespace | onnx |
| Namespace for the ONNX parser of the dlinear library. | |
| namespace | qsopt_ex |
| namespace | smt2 |
| Namespace for the SMT2 parser of the dlinear library. | |
| namespace | vnnlib |
| Namespace for the VNNLIB parser of the dlinear library. | |
Classes | |
| class | ArgParser |
| Used to parse command line arguments and produce a corresponding Config object to be used throughout the execution. More... | |
| class | BitIncrementIterator |
| BitIncrementIterator class. More... | |
| struct | Bound |
| Tuple containing the value, bound type and theory literal associated with the bound. More... | |
| class | BoundImplicator |
| Use theory reasoning to add relations between literals using some simple theory inferences. More... | |
| class | BoundIterator |
| BoundIterator class. More... | |
| class | BoundPreprocessor |
| This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver. More... | |
| class | BoundVector |
| Data structure to store the LP solver bounds in a sorted vector to determine the active lower and upper bound for the column. More... | |
| class | Box |
| Collection of variables with associated intervals. More... | |
| class | CadicalSatSolver |
| SAT solver based on CaDiCal. More... | |
| class | CompleteSoplexTheorySolver |
| Complete solver using SoPlex. More... | |
| class | Config |
| Simple dataclass used to store the configuration of the program. More... | |
| class | Context |
| Context class that holds the set of constraints and provide Assert/Push/Pop/CheckSat functionalities. More... | |
| class | DeltaQsoptexTheorySolver |
| Delta complete solver using QSopt_ex. More... | |
| class | DeltaSoplexTheorySolver |
| Delta complete solver using SoPlex. More... | |
| class | Driver |
| The Driver is the base class for all the parsers. More... | |
| struct | EdgeEqual_ |
| struct | EdgeHash_ |
| class | ExpressionEvaluator |
| Evaluate an expression with a given box. More... | |
| class | FormulaVisitor |
| This base class provides all the methods expected to visit the underlying formula and return a modified version. More... | |
| class | GenericExpressionVisitor |
| Generic expression visitor implementing the visitor pattern. More... | |
| class | GenericFormulaVisitor |
| Generic formula visitor implementing the visitor pattern. More... | |
| class | Graph |
| Graph class. More... | |
| class | IfThenElseEliminator |
| IfThenElseEliminator class. More... | |
| class | Infinity |
| Global class storing the infinity values for the different LP solvers. More... | |
| class | Interval |
| class | IterationStats |
| Dataclass collecting statistics about some operation or process. More... | |
| class | LeakyReluConstraint |
| class | LinearFormulaFlattener |
| Used by the PredicateAbstractor to ensure that all the theory literals are in the flattened standard form. More... | |
| struct | Literal |
| A literal is a variable with an associated truth value, indicating whether it is true or false. More... | |
| class | NaiveCnfizer |
Transforms a symbolic formula f into a CNF formula by preserving its semantics. More... | |
| class | Nnfizer |
| Implementation of NNF (Negation Normal Form) conversion. More... | |
| class | NNSoplexTheorySolver |
| Specialised theory solver for neural networks using SoPlex. More... | |
| struct | NumericDataContainer |
| NumericDataContainer class. More... | |
| class | OptionValue |
| Represents an optional value in dLinear. More... | |
| class | PicosatSatSolver |
| PicoSAT is a SAT solver written in C. More... | |
| class | PiecewiseLinearConstraint |
| A piecewise linear constraint is a constraint that assumes different linear functions depending on the truth assignment of a literal. More... | |
| class | PlaistedGreenbaumCnfizer |
| Plaisted-Greenbaum transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF. More... | |
| class | PredicateAbstractor |
| Predicate abstraction is a method to convert a first-order logic formula into a Boolean formula. More... | |
| class | PrefixPrinter |
| Print expressions and formulas in prefix-form. More... | |
| class | QsoptexTheorySolver |
| QSopt_ex is an exact LP solver written in C. More... | |
| class | ReluConstraint |
| A ReLU constraint is a kind of piecewise linear constraint. More... | |
| class | RoundingModeGuard |
| class | SatSolver |
| Base class for SAT solvers. More... | |
| class | ScopedUnorderedMap |
| class | ScopedUnorderedSet |
| class | ScopedVector |
| class | SmtSolver |
| This class provides an easy interface for using the underling solver. More... | |
| struct | SmtSolverOutput |
| Data struct containing the output of the solver, such as the result of the computation as well as some statistics. More... | |
| class | SoplexTheorySolver |
| SoPlex is an exact LP solver written in C++. More... | |
| class | SortedVector |
| Vector that maintains its elements sorted. More... | |
| class | Stats |
| Dataclass collecting statistics about some operation or process. More... | |
| class | TheorySolver |
| Base class for theory solvers. More... | |
| class | Timer |
| Timer class using the a steady clock. More... | |
| class | TimerBase |
| Simple timer class to evaluate the performance of the software. More... | |
| class | TimerGuard |
| The TimeGuard wraps a timer object and pauses it when the guard object is destructed. More... | |
| class | TseitinCnfizer |
| Tsietin transformation is a method to convert a formula into an equi-satisfiable vector of formulae in CNF. More... | |
| struct | user_clock |
| class | UserTimer |
| Timer class using the user_clock. More... | |
Concepts | |
| concept | IsAnyOf |
| Check if the type T is any of the types U. | |
| concept | IsNotAnyOf |
| Check if the type T is not any of the types U. | |
| concept | Arithmetic |
| Check if the type T supports the arithmetic operations +, -, *, /. | |
| concept | Numeric |
| Check if the type T supports the arithmetic operations +, -, *, / and the comparison operators <, >, <=, >=. | |
Typedefs | |
| using | LiteralSet = std::set<Literal> |
| A set of literals. | |
| using | Model = std::pair<std::vector<Literal>, std::vector<Literal>> |
| A model is a pair of two vectors of literals. | |
Enumerations | |
| enum class | Logic { QF_NRA , QF_NRA_ODE , QF_LRA , QF_RDL , QF_LIA , LRA } |
| The SMT-LIB logic the SMT2 file is using. More... | |
| enum class | LpColBound { L = 0 , SL = 1 , B = 2 , SU = 3 , U = 4 , D = 5 , F = 6 } |
| Describe the bound of a linear program variable. More... | |
| enum class | LpResult { LP_NO_RESULT , LP_UNSOLVED , LP_INFEASIBLE , LP_UNBOUNDED , LP_OPTIMAL , LP_DELTA_OPTIMAL } |
| Result of running the LP solver over the input problem. More... | |
| enum class | LpRowSense { LT = 0 , EQ = 1 , LE = 2 , GE , GT , NQ , IN } |
| Sense of a linear programming row describing a constraint. More... | |
| enum class | PiecewiseConstraintState { NOT_FIXED , INACTIVE , ACTIVE } |
| State a piecewise constraint can be in. More... | |
| enum class | SatResult { SAT_NO_RESULT , SAT_UNSOLVED , SAT_UNSATISFIABLE , SAT_SATISFIABLE , SAT_DELTA_SATISFIABLE } |
| Result of running the theory solver over the literals decided by the SAT solver. More... | |
| enum class | SmtResult { UNSOLVED , SKIP_SAT , SAT , DELTA_SAT , OPTIMAL , DELTA_OPTIMAL , UNBOUNDED , INFEASIBLE , UNSAT , UNKNOWN , ERROR } |
| SmtSolver Result based on the result of the solver. More... | |
| enum class | RelationalOperator { EQ , NEQ , GT , GEQ , LT , LEQ } |
| Relational operators are used in formulas. More... | |
| enum class | VisitResult { CONTINUE , SKIP , STOP } |
| Result returned by the visit function. More... | |
Functions | |
| Logic | parseLogic (const std::string &s) |
| Parse the logic from a string. | |
| char | toChar (LpColBound bound) |
| Convert the bound to a character. | |
| LpColBound | operator! (LpColBound bound) |
| Invert the bound with delta == 0. | |
| LpColBound | operator- (LpColBound bound) |
| Invert the bound with delta > 0. | |
| LpColBound | operator~ (LpColBound bound) |
| Relax the bound. | |
| LpColBound | parseLpBound (char bound) |
| Parse the bound from a character. | |
| LpColBound | relax (LpColBound bound) |
| Relax the bound. | |
| LpColBound | invert (LpColBound bound, bool delta) |
| Invert the bound. | |
| LpResult | parseLpResult (int res) |
| Parse the result from the returned integer. | |
| LpRowSense | parseLpSense (const Formula &f) |
| Parse the sense from a formula. | |
| LpRowSense | parseLpSense (char sense) |
| Parse the sense from a character. | |
| char | toChar (LpRowSense sense) |
| Convert the sense to a character. | |
| LpRowSense | operator! (LpRowSense sense) |
| Invert the sense with delta == 0. | |
| LpRowSense | operator- (LpRowSense sense) |
| Invert the sense with delta > 0. | |
| LpRowSense | operator~ (LpRowSense sense) |
| Relax the sense, assuming delta > 0.e. | |
| std::string | ToPrefix (const Expression &e) |
Produce the prefix-string representation of the expression e. | |
| std::string | ToPrefix (const Formula &f) |
Produce the prefix-string representation of the formula f. | |
| FormulaKind | operator- (FormulaKind kind) |
| Change the kind of the formula by multiplying all the expressions by a negative number. | |
| Formula | imply (const Formula &f1, const Formula &f2) |
Return a formula f1 ⇒ f2. | |
| Formula | imply (const Variable &v, const Formula &f) |
Return a formula v ⇒ f. | |
| Formula | imply (const Formula &f, const Variable &v) |
Return a formula f ⇒ v. | |
| Formula | imply (const Variable &v1, const Variable &v2) |
Return a formula v1 ⇒ v2. | |
| Formula | iff (const Formula &f1, const Formula &f2) |
Return a formula f1 ⇔ f2. | |
| Formula | iff (const Variable &v, const Formula &f) |
Return a formula v ⇔ f. | |
| Formula | iff (const Formula &f, const Variable &v) |
Return a formula f ⇔ v. | |
| Formula | iff (const Variable &v1, const Variable &v2) |
Return a formula v1 ⇔ v2. | |
| std::set< Formula > | map (const std::set< Formula > &formulas, const std::function< Formula(const Formula &)> &func) |
Given formulas = {f₁, ..., fₙ} and a func : Formula → Formula, map(formulas, func) returns a set {func(f₁), ... func(fₙ)}. | |
| bool | is_atomic (const Formula &f) |
Check if f is atomic. | |
| bool | is_clause (const Formula &f) |
Check if f is a clause. | |
| std::set< Formula > | get_clauses (const Formula &f) |
| Returns the set of clauses in f. | |
| bool | is_cnf (const Formula &f) |
Check if f is in CNF form. | |
| bool | HaveIntersection (const Variables &variables1, const Variables &variables2) |
Check if the intersection of variables1 and variables2 is non-empty. | |
| Formula | DeltaStrengthen (const Formula &f, const double delta) |
Strengthen the input formula $p f by delta. | |
| Formula | DeltaWeaken (const Formula &f, const double delta) |
Weaken the input formula $p f by delta. | |
| bool | IsDifferentiable (const Formula &f) |
Check if the formula f is symbolic-differentiable. | |
| bool | IsDifferentiable (const Expression &e) |
| Check if the expression f is symbolic-differentiable. | |
| Formula | make_conjunction (const std::vector< Formula > &formulas) |
Make conjunction of formulas. | |
| Formula | make_disjunction (const std::vector< Formula > &formulas) |
Make disjunction of formulas. | |
| std::vector< Variable > | CreateVector (const std::string &prefix, int size, Variable::Type type=Variable::Type::CONTINUOUS) |
Creates a vector of variables of type whose size is size. | |
| RelationalOperator | operator! (RelationalOperator op) |
Negates op. | |
| std::string | GetExtension (const std::string &name) |
| Get the extension of the file. | |
| std::vector< std::string > | SplitStringByWhitespace (const char *in) |
| Split a C-string by whitespace. | |
| std::vector< std::string > | GetFiles (const std::string &path, const std::string &extension="") |
| Get the files in a directory. | |
| bool | IsInteger (double v) |
Returns true if v is represented by int. | |
| bool | IsInteger (const mpq_class &v) |
Check if v is represented by int. | |
| int | ConvertInt64ToInt (std::int64_t v) |
Convert v of int64_t to int. | |
| double | ConvertInt64ToDouble (std::int64_t v) |
Convert v of int64_t to double. | |
| mpq_class | ConvertInt64ToRational (std::int64_t v) |
Convert v of int64_t to rational. | |
Global namespace for the dlinear library.
BoundIterator class.
This class is used to propagate some simple theory inferences in the SAT solver. E.g.
\[ x \le 10 \implies x < 4 \newline x < 2 \implies \neg (x = 8) \]
It is used to iterate over the bounds of a theory solver without copying each dlinear::BoundVector::Bound. Usually the results of bound violation.
This class uses some basic algebraic operations to preprocess the constraints and identify violations before invoking the solver. Namely, the bounds are propagated through the constraints.
The LP solver used is Soplex. This solver is complete. It means that it will always solve the linear problem exactly.
Neural network theory solver using SoPlex.
The class provides all the methods expected to visit the underlying formula and return a modified version. By default, the visitor returns the original formula, but it can be overridden by the derived classes.
Used by the dlinear::PredicateAbstractor to ensure that all the theory literals are in the flattened standard form.
Literals are a pair formed by a boolean variable and a truth value indicating whether the variable is negated or not.
Other files in dlinear should include this file and should NOT include files in drake/common directory. Similarly, BUILD files should only have a dependency "//dlinear/symbolic:symbolic", not "@drake_symbolic//:symbolic".
It implements an abstraction used to iterate over all the possible bit vectors of a given size.
Concepts have been introduced in the c++20 standard and are used in the dlinear library in order to make the code more readable and to provide better error messages in templated code.
Simple dataclass used to store the configuration of the program. It is generated from dlinear::ArgParser.
Simple utilities that make operations on the filesystem easier.
Generic graph implementation that can be used to represent a graph with vertices of type T.
An interval assigned to a variable describes the range of values it can assume.
The verbosity level is set with the -V flag. The verbosity level is an integer between 0 and 5 and it increases with each -V flag. It can be reduced with the -q flag. It starts at 2 (warning).
Simple class that holds a numeric value and a data value. It is used to take advantage of the strong ordering and equality operators of the numeric value, as well as the arithmetic operators, while still being able to store additional data.
It is used to wrap a value that can be set from multiple sources. The value is overwritten only if it is not set from a higher priority source. The priority is defined as follows, where the higher the number, the higher the priority:
This is a unordered_set that supports backtracking. It is used to store intermediate results.
This is a vector that supports backtracking. It is used to store intermediate results.
|
strong |
The SMT-LIB logic the SMT2 file is using.
|
strong |
Describe the bound of a linear program variable.
If the bound is strict, it means that the variable cannot assume the bound value. When using delta complete solvers, strict bounds can be relaxed to non-strict bounds.
| Enumerator | |
|---|---|
| L | Lower bound. |
| SL | Strict lower bound. |
| B | Both upper and lower bound are equal (fixed) |
| SU | Strict upper bound. |
| U | Upper bound. |
| D | Variable must be different from the bound. |
| F | Free variable. |
Definition at line 21 of file LpColBound.h.
|
strong |
Result of running the LP solver over the input problem.
Definition at line 14 of file LpResult.h.
|
strong |
Sense of a linear programming row describing a constraint.
If the sense is strict, it means that the variable cannot assume the right-hand-side value. When using delta complete solvers, strict senses can be relaxed to non-strict senses.
| Enumerator | |
|---|---|
| LT | Less than. |
| EQ | Equal to. |
| LE | Less than or equal to. |
| GE | Greater than or equal to. |
| GT | Greater than. |
| NQ | Not equal to. |
| IN | Inactive. |
Definition at line 23 of file LpRowSense.h.
|
strong |
State a piecewise constraint can be in.
| Enumerator | |
|---|---|
| NOT_FIXED | The constraint is not fixed yet. |
| INACTIVE | The constraint is inactive. |
| ACTIVE | The constraint is active. |
Definition at line 14 of file PiecewiseConstraintState.h.
|
strong |
Relational operators are used in formulas.
| Enumerator | |
|---|---|
| EQ | = |
| NEQ | != |
| GT |
|
| GEQ | >= |
| LT | < |
| LEQ | <= |
Definition at line 191 of file symbolic.h.
|
strong |
Result of running the theory solver over the literals decided by the SAT solver.
It describes the result the solver was able to produce on the input problem for the current iteration.
Definition at line 17 of file SatResult.h.
|
strong |
SmtSolver Result based on the result of the solver.
Definition at line 24 of file SmtSolverOutput.h.
|
strong |
Result returned by the visit function.
Depending on the result, the search algorithm will continue, skip adding the adjacent vertices to the stack/queue, or stop the search altogether.
| double dlinear::ConvertInt64ToDouble | ( | std::int64_t | v | ) |
| int dlinear::ConvertInt64ToInt | ( | std::int64_t | v | ) |
| mpq_class dlinear::ConvertInt64ToRational | ( | std::int64_t | v | ) |
| std::vector< Variable > dlinear::CreateVector | ( | const std::string & | prefix, |
| int | size, | ||
| Variable::Type | type = Variable::Type::CONTINUOUS ) |
Creates a vector of variables of type whose size is size.
The variables are numbered with prefix. For example
| prefix | prefix of variable names. Must not be empty. |
| size | size of vector. Must be >= 1. |
| type | type of variables |
Definition at line 501 of file symbolic.cpp.
Strengthen the input formula $p f by delta.
Strengthen the input formula f by delta.
| f | formula to strengthen |
| delta | amount to strengthen by |
Definition at line 470 of file symbolic.cpp.
Weaken the input formula $p f by delta.
Weaken the input formula f by delta.
| f | formula to weaken |
| delta | amount to weaken by |
Definition at line 476 of file symbolic.cpp.
Returns the set of clauses in f.
F is assumed to be in CNF. That is, f is either a single clause or a conjunction of clauses.
| f | formula to get clauses from |
f Definition at line 98 of file symbolic.cpp.
| std::string dlinear::GetExtension | ( | const std::string & | name | ) |
Get the extension of the file.
Extracts the extension from name, meaning the part of the file name after the last dot.
name. | name | The name of the file. |
Definition at line 16 of file filesystem.cpp.
| std::vector< std::string > dlinear::GetFiles | ( | const std::string & | path, |
| const std::string & | extension = "" ) |
Get the files in a directory.
| path | The path to the directory. |
Definition at line 35 of file filesystem.cpp.
Check if the intersection of variables1 and variables2 is non-empty.
| variables1 | set of variables |
| variables2 | set of variables |
variables1 and variables2 is an non-empty intersection. Definition at line 126 of file symbolic.cpp.
|
inline |
Invert the bound.
Depending on whether the value of delta is > 0 or not, there are two possible conversion:
| bound | bound to invert |
| delta | whether delta is greater than 0 |
Definition at line 92 of file LpColBound.h.
| bool dlinear::is_atomic | ( | const Formula & | f | ) |
Check if f is atomic.
| f | formula to check |
f is atomic Definition at line 53 of file symbolic.cpp.
| bool dlinear::is_clause | ( | const Formula & | f | ) |
Check if f is a clause.
A clause is a disjunction of literals.
| f | formula to check |
f is a clause Definition at line 78 of file symbolic.cpp.
| bool dlinear::is_cnf | ( | const Formula & | f | ) |
Check if f is in CNF form.
| f | formula to check |
f is in CNF form Definition at line 110 of file symbolic.cpp.
| bool dlinear::IsDifferentiable | ( | const Expression & | e | ) |
Check if the expression f is symbolic-differentiable.
| e | expression to check |
e is symbolic-differentiable Definition at line 483 of file symbolic.cpp.
| bool dlinear::IsDifferentiable | ( | const Formula & | f | ) |
Check if the formula f is symbolic-differentiable.
| f | formula to check |
f is symbolic-differentiable Definition at line 481 of file symbolic.cpp.
| bool dlinear::IsInteger | ( | const mpq_class & | v | ) |
| bool dlinear::IsInteger | ( | double | v | ) |
Make conjunction of formulas.
std::vector<Formula> while Drake's version takes std::set<Formula>. | formulas | input formulas |
formulas Definition at line 485 of file symbolic.cpp.
Make disjunction of formulas.
std::vector<Formula> while Drake's version takes std::set<Formula>. | formulas | input formulas |
formulas Definition at line 493 of file symbolic.cpp.
| std::set< Formula > dlinear::map | ( | const std::set< Formula > & | formulas, |
| const std::function< Formula(const Formula &)> & | func ) |
Given formulas = {f₁, ..., fₙ} and a func : Formula → Formula, map(formulas, func) returns a set {func(f₁), ... func(fₙ)}.
| formulas | set of formulas |
| func | function to apply to each formula |
func to each formula in Definition at line 47 of file symbolic.cpp.
| LpColBound dlinear::operator! | ( | LpColBound | bound | ) |
Invert the bound with delta == 0.
More specifically, !U == SL, !SU == L, !B == D, !D == B, !IN == IN, !L == SU, !SL == U.
| bound | bound to invert |
Definition at line 54 of file LpColBound.cpp.
| LpRowSense dlinear::operator! | ( | LpRowSense | sense | ) |
Invert the sense with delta == 0.
More specifically, !LE == GT, !GE == LT, !EQ == NQ, !NQ == EQ, !IN == IN, !GT == LE, !LT == GE.
| sense | sense to invert |
Definition at line 68 of file LpRowSense.cpp.
| RelationalOperator dlinear::operator! | ( | RelationalOperator | op | ) |
Negates op.
| op | operator to negate |
Definition at line 512 of file symbolic.cpp.
| FormulaKind dlinear::operator- | ( | FormulaKind | kind | ) |
Change the kind of the formula by multiplying all the expressions by a negative number.
In practice this inverts the inequality from \( < \) to \( > \) and \( \leq \) to \( \geq \) and vice versa.
| kind | kind of the formula |
Definition at line 19 of file symbolic.cpp.
| LpColBound dlinear::operator- | ( | LpColBound | bound | ) |
Invert the bound with delta > 0.
More specifically, -U == L, -L == U, -B == F, -F == B. Any other bound generates an assertion error
| bound | bound to invert |
Definition at line 73 of file LpColBound.cpp.
| LpRowSense dlinear::operator- | ( | LpRowSense | sense | ) |
Invert the sense with delta > 0.
More specifically, -LE == GT, -GE == LE, -EQ == NQ, -NQ == EQ. Any other sense generates an assertion error
| sense | sense to invert |
Definition at line 89 of file LpRowSense.cpp.
| LpColBound dlinear::operator~ | ( | LpColBound | bound | ) |
Relax the bound.
More specifically, ~SL == L, ~SU == U, ~D == F. Any other bound remain unchanged.
| bound | bound to relax |
Definition at line 88 of file LpColBound.cpp.
| LpRowSense dlinear::operator~ | ( | LpRowSense | sense | ) |
Relax the sense, assuming delta > 0.e.
More specifically, LT -> LE, GT -> GE. The other senses remain unchanged.
| sense | sense to relax |
Definition at line 104 of file LpRowSense.cpp.
| Logic dlinear::parseLogic | ( | const std::string & | s | ) |
| LpColBound dlinear::parseLpBound | ( | char | bound | ) |
Parse the bound from a character.
| bound | character to parse |
| LpResult dlinear::parseLpResult | ( | int | res | ) |
Parse the result from the returned integer.
| res | return code |
| LpRowSense dlinear::parseLpSense | ( | char | sense | ) |
Parse the sense from a character.
| sense | character to parse |
Definition at line 23 of file LpRowSense.cpp.
| LpRowSense dlinear::parseLpSense | ( | const Formula & | f | ) |
Parse the sense from a formula.
| f | formula to parse |
Definition at line 12 of file LpRowSense.cpp.
|
inline |
Relax the bound.
More specifically, ~SL == L, ~SU == U, ~D == F. Any other bound remain unchanged.
| bound | bound to relax |
Definition at line 79 of file LpColBound.h.
| std::vector< std::string > dlinear::SplitStringByWhitespace | ( | const char * | in | ) |
Split a C-string by whitespace.
Each word is returned as a separate string in a vector.
| in | input string to split |
Definition at line 22 of file filesystem.cpp.
| char dlinear::toChar | ( | LpColBound | bound | ) |
Convert the bound to a character.
| bound | bound to convert |
Definition at line 33 of file LpColBound.cpp.
| char dlinear::toChar | ( | LpRowSense | sense | ) |
Convert the sense to a character.
| sense | sense to convert |
Definition at line 47 of file LpRowSense.cpp.
| std::string dlinear::ToPrefix | ( | const Expression & | e | ) |
Produce the prefix-string representation of the expression e.
| e | expression to convert |
Definition at line 242 of file PrefixPrinter.cpp.
| std::string dlinear::ToPrefix | ( | const Formula & | f | ) |
Produce the prefix-string representation of the formula f.
| f | formula to convert |
Definition at line 251 of file PrefixPrinter.cpp.
1.11.0