carl::vs::detail Namespace Reference
Data Structures | |
| struct | Substitution |
Typedefs | |
| using | DoubleInterval = carl::Interval< double > |
| using | EvalDoubleIntervalMap = std::map< carl::Variable, DoubleInterval > |
Functions | |
| template<class Poly > | |
| std::ostream & | operator<< (std::ostream &os, const Substitution< Poly > &s) |
| template<class combineType > | |
| bool | combine (const std::vector< std::vector< std::vector< combineType > > > &_toCombine, std::vector< std::vector< combineType > > &_combination) |
| Combines vectors. More... | |
| template<typename Poly > | |
| void | simplify (CaseDistinction< Poly > &) |
| Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. More... | |
| template<typename Poly > | |
| void | simplify (CaseDistinction< Poly > &, carl::Variables &, const detail::EvalDoubleIntervalMap &) |
| Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. More... | |
| template<typename Poly > | |
| bool | splitProducts (CaseDistinction< Poly > &, bool=false) |
| Splits all constraints in the given disjunction of conjunctions of constraints having a non-trivial factorization into a set of constraints which compare the factors instead. More... | |
| template<typename Poly > | |
| bool | splitProducts (const ConstraintConjunction< Poly > &, CaseDistinction< Poly > &, std::map< const Constraint< Poly >, CaseDistinction< Poly >> &, bool=false) |
| Splits all constraints in the given conjunction of constraints having a non-trivial factorization into a set of constraints which compare the factors instead. More... | |
| template<typename Poly > | |
| CaseDistinction< Poly > | splitProducts (const Constraint< Poly > &, bool=false) |
| Splits the given constraint into a set of constraints which compare the factors of the factorization of the constraints considered polynomial. More... | |
| template<typename Poly > | |
| void | splitSosDecompositions (CaseDistinction< Poly > &) |
| template<typename Poly > | |
| CaseDistinction< Poly > | getSignCombinations (const Constraint< Poly > &) |
| For a given constraint f_1*...*f_n ~ 0 this method computes all combinations of constraints f_1 ~_1 0 ... More... | |
| void | getOddBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings) |
| void | getEvenBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings) |
| template<typename Poly > | |
| void | print (CaseDistinction< Poly > &_substitutionResults) |
| Prints the given disjunction of conjunction of constraints. More... | |
| template<typename Poly > | |
| bool | substitute (const Constraint< Poly > &, const Substitution< Poly > &, CaseDistinction< Poly > &, bool _accordingPaper, carl::Variables &, const detail::EvalDoubleIntervalMap &) |
| Applies a substitution to a constraint and stores the results in the given vector. More... | |
| template<typename Poly > | |
| bool | substituteNormal (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, CaseDistinction< Poly > &_result, bool _accordingPaper, carl::Variables &_conflictingVariables, const detail::EvalDoubleIntervalMap &_solutionSpace) |
| Applies a substitution of a variable to a term, which is not minus infinity nor a to an square root expression plus an infinitesimal. More... | |
| template<typename Poly > | |
| bool | substituteNormalSqrtEq (const Poly &_radicand, const Poly &_q, const Poly &_r, CaseDistinction< Poly > &_result, bool _accordingPaper) |
| Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More... | |
| template<typename Poly > | |
| bool | substituteNormalSqrtNeq (const Poly &_radicand, const Poly &_q, const Poly &_r, CaseDistinction< Poly > &_result, bool _accordingPaper) |
| Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More... | |
| template<typename Poly > | |
| bool | substituteNormalSqrtLess (const Poly &_radicand, const Poly &_q, const Poly &_r, const Poly &_s, CaseDistinction< Poly > &_result, bool _accordingPaper) |
| Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More... | |
| template<typename Poly > | |
| bool | substituteNormalSqrtLeq (const Poly &_radicand, const Poly &_q, const Poly &_r, const Poly &_s, CaseDistinction< Poly > &_result, bool _accordingPaper) |
| Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More... | |
| template<typename Poly > | |
| bool | substitutePlusEps (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, CaseDistinction< Poly > &_result, bool _accordingPaper, carl::Variables &_conflictingVariables, const detail::EvalDoubleIntervalMap &_solutionSpace) |
| Applies the given substitution to the given constraint, where the substitution is of the form [x -> t+epsilon] with x as the variable and c and b polynomials in the real theory excluding x. More... | |
| template<typename Poly > | |
| bool | substituteEpsGradients (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, const carl::Relation _relation, CaseDistinction< Poly > &, bool _accordingPaper, carl::Variables &_conflictingVariables, const detail::EvalDoubleIntervalMap &_solutionSpace) |
| Sub-method of substituteEps, where one of the gradients in the point represented by the substitution must be negative if the given relation is less or positive if the given relation is greater. More... | |
| template<typename Poly > | |
| void | substituteInf (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, CaseDistinction< Poly > &_result, carl::Variables &_conflictingVariables, const detail::EvalDoubleIntervalMap &_solutionSpace) |
| Applies the given substitution to the given constraint, where the substitution is of the form [x -> -infinity] with x as the variable and c and b polynomials in the real theory excluding x. More... | |
| template<typename Poly > | |
| void | substituteInfLessGreater (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, CaseDistinction< Poly > &_result) |
| Applies the given substitution to the given constraint, where the substitution is of the form [x -> +/-infinity] with x as the variable and c and b polynomials in the real theory excluding x. More... | |
| template<typename Poly > | |
| void | substituteTrivialCase (const Constraint< Poly > &_cons, const Substitution< Poly > &_subs, CaseDistinction< Poly > &_result) |
| Deals with the case, that the left hand side of the constraint to substitute is a trivial polynomial in the variable to substitute. More... | |
| template<typename Poly > | |
| void | substituteNotTrivialCase (const Constraint< Poly > &, const Substitution< Poly > &, CaseDistinction< Poly > &) |
| Deals with the case, that the left hand side of the constraint to substitute is not a trivial polynomial in the variable to substitute. More... | |
Typedef Documentation
◆ DoubleInterval
| using carl::vs::detail::DoubleInterval = typedef carl::Interval<double> |
Definition at line 51 of file substitute.h.
◆ EvalDoubleIntervalMap
| using carl::vs::detail::EvalDoubleIntervalMap = typedef std::map<carl::Variable, DoubleInterval> |
Definition at line 52 of file substitute.h.
Function Documentation
◆ combine()
template<class combineType >
|
inline |
Combines vectors.
- Parameters
-
_toCombine The vectors to combine. _combination The resulting combination.
- Returns
- false, if the upper limit in the number of combinations resulting by this method is exceeded. Note, that this hinders a combinatorial blow up. true, otherwise.
◆ getEvenBitStrings()
|
inline |
- Parameters
-
_length The maximal length of the bit strings with even parity to compute. _strings All bit strings of length less or equal the given length with even parity.
◆ getOddBitStrings()
|
inline |
- Parameters
-
_length The maximal length of the bit strings with odd parity to compute. _strings All bit strings of length less or equal the given length with odd parity.
◆ getSignCombinations()
template<typename Poly >
|
inline |
For a given constraint f_1*...*f_n ~ 0 this method computes all combinations of constraints f_1 ~_1 0 ...
f_n ~_n 0 such that
f_1 ~_1 0 and ... and f_n ~_n 0 iff f_1*...*f_n ~ 0
holds.
- Parameters
-
_constraint A pointer to the constraint to split this way.
- Returns
- The resulting combinations.
◆ operator<<()
template<class Poly >
|
inline |
◆ print()
template<typename Poly >
|
inline |
Prints the given disjunction of conjunction of constraints.
- Parameters
-
_substitutionResults The disjunction of conjunction of constraints to print.
Here is the caller graph for this function:
◆ simplify() [1/2]
template<typename Poly >
|
inline |
Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints.
If a conjunction of only consistent constraints exists, the simplified disjunction contains one empty conjunction.
- Parameters
-
_toSimplify The disjunction of conjunctions to simplify.
◆ simplify() [2/2]
template<typename Poly >
|
inline |
Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints.
If a conjunction of only consistent constraints exists, the simplified disjunction contains one empty conjunction.
- Parameters
-
_toSimplify The disjunction of conjunctions to simplify. _conflictingVars _solutionSpace
◆ splitProducts() [1/3]
template<typename Poly >
|
inline |
Splits all constraints in the given disjunction of conjunctions of constraints having a non-trivial factorization into a set of constraints which compare the factors instead.
- Parameters
-
_toSimplify The disjunction of conjunctions of the constraints to split. _onlyNeq A flag indicating that only constraints with the relation symbol != are split.
- Returns
- false, if the upper limit in the number of combinations resulting by this method is exceeded. Note, that this hinders a combinatorial blow up. true, otherwise.
Here is the caller graph for this function:
◆ splitProducts() [2/3]
template<typename Poly >
|
inline |
Splits the given constraint into a set of constraints which compare the factors of the factorization of the constraints considered polynomial.
- Parameters
-
_constraint A pointer to the constraint to split. _onlyNeq A flag indicating that only constraints with the relation symbol != are split.
- Returns
- The resulting disjunction of conjunctions of constraints, which is semantically equivalent to the given constraint.
◆ splitProducts() [3/3]
template<typename Poly >
|
inline |
Splits all constraints in the given conjunction of constraints having a non-trivial factorization into a set of constraints which compare the factors instead.
- Parameters
-
_toSimplify The conjunction of the constraints to split. _result The result, being a disjunction of conjunctions of constraints. _onlyNeq A flag indicating that only constraints with the relation symbol != are split.
- Returns
- false, if the upper limit in the number of combinations resulting by this method is exceeded. Note, that this hinders a combinatorial blow up. true, otherwise.
◆ splitSosDecompositions()
template<typename Poly >
|
inline |
Here is the caller graph for this function:
◆ substitute()
template<typename Poly >
|
inline |
Applies a substitution to a constraint and stores the results in the given vector.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution.
- Returns
- false, if the upper limit in the number of combinations in the result of the substitution is exceeded. Note, that this hinders a combinatorial blow up. true, otherwise.
Here is the caller graph for this function:
◆ substituteEpsGradients()
template<typename Poly >
|
inline |
Sub-method of substituteEps, where one of the gradients in the point represented by the substitution must be negative if the given relation is less or positive if the given relation is greater.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _relation The relation symbol, deciding whether the substitution result must be negative or positive. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false). _conflictingVariables If a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container. _solutionSpace The solution space in form of double intervals of the variables occurring in the given constraint.
◆ substituteInf()
template<typename Poly >
|
inline |
Applies the given substitution to the given constraint, where the substitution is of the form [x -> -infinity] with x as the variable and c and b polynomials in the real theory excluding x.
The constraint is of the form "f(x) \rho 0" with \rho element of {=,!=,<,>,<=,>=} and k as the maximum degree of x in f.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _conflictingVariables If a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container. _solutionSpace The solution space in form of double intervals of the variables occurring in the given constraint.
◆ substituteInfLessGreater()
template<typename Poly >
|
inline |
Applies the given substitution to the given constraint, where the substitution is of the form [x -> +/-infinity] with x as the variable and c and b polynomials in the real theory excluding x.
The constraint is of the form "a*x^2+bx+c \rho 0", where \rho is less or greater.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
◆ substituteNormal()
template<typename Poly >
|
inline |
Applies a substitution of a variable to a term, which is not minus infinity nor a to an square root expression plus an infinitesimal.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false). _conflictingVariables If a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container. _solutionSpace The solution space in form of double intervals of the variables occurring in the given constraint.
◆ substituteNormalSqrtEq()
template<typename Poly >
|
inline |
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root.
The relation symbol of the constraint to substitute is "=".
(_q+_r*sqrt(_radicand))
The term then looks like: ---------------— _s
- Parameters
-
_radicand The radicand of the square root. _q The summand not containing the square root. _r The coefficient of the radicand. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false).
◆ substituteNormalSqrtLeq()
template<typename Poly >
|
inline |
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root.
The relation symbol of the constraint to substitute is less or equal.
(_q+_r*sqrt(_radicand))
The term then looks like: -------------------— _s
- Parameters
-
_radicand The radicand of the square root. _q The summand not containing the square root. _r The coefficient of the radicand. _s The denominator of the expression containing the square root. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false).
◆ substituteNormalSqrtLess()
template<typename Poly >
|
inline |
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root.
The relation symbol of the constraint to substitute is less.
(_q+_r*sqrt(_radicand))
The term then looks like: -------------------— _s
- Parameters
-
_radicand The radicand of the square root. _q The summand not containing the square root. _r The coefficient of the radicand. _s The denominator of the expression containing the square root. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false).
◆ substituteNormalSqrtNeq()
template<typename Poly >
|
inline |
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root.
The relation symbol of the constraint to substitute is "!=".
(_q+_r*sqrt(_radicand))
The term then looks like: --------------------— _s
- Parameters
-
_radicand The radicand of the square root. _q The summand not containing the square root. _r The coefficient of the radicand. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false).
◆ substituteNotTrivialCase()
template<typename Poly >
|
inline |
Deals with the case, that the left hand side of the constraint to substitute is not a trivial polynomial in the variable to substitute.
The constraints left hand side then should looks like: ax^2+bx+c
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
◆ substitutePlusEps()
template<typename Poly >
|
inline |
Applies the given substitution to the given constraint, where the substitution is of the form [x -> t+epsilon] with x as the variable and c and b polynomials in the real theory excluding x.
The constraint is of the form "f(x) \rho 0" with \rho element of {=,!=,<,>,<=,>=} and k as the maximum degree of x in f.
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints. _accordingPaper A flag that indicates whether to apply the virtual substitution rules according to the paper "Quantifier elimination for real algebra - the quadratic case and beyond." by Volker Weispfenning (true) or in an adapted way which omits a higher degree in the result by splitting the result in more cases (false). _conflictingVariables If a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container. _solutionSpace The solution space in form of double intervals of the variables occurring in the given constraint.
◆ substituteTrivialCase()
template<typename Poly >
|
inline |
Deals with the case, that the left hand side of the constraint to substitute is a trivial polynomial in the variable to substitute.
The constraints left hand side then should look like: ax^2+bx+c
- Parameters
-
_cons The constraint to substitute in. _subs The substitution to apply. _result The vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
