SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Structures | Typedefs | Functions
smtrat::vs Namespace Reference

Data Structures

class  Condition
 
struct  unsignedTripleCmp
 
class  State
 
class  Substitution
 
struct  substitutionPointerEqual
 
struct  substitutionPointerHash
 

Typedefs

typedef std::set< carl::PointerSet< Condition > > ConditionSetSet
 
typedef std::set< ConditionSetSet > ConditionSetSetSet
 
typedef std::list< const Condition * > ConditionList
 
typedef std::vector< ConditionList > DisjunctionOfConditionConjunctions
 
typedef std::pair< size_t, std::pair< size_t, size_t > > UnsignedTriple
 
typedef std::pair< UnsignedTriple, vs::State * > ValStatePair
 
typedef std::map< UnsignedTriple, vs::State *, unsignedTripleCmp > ValuationMap
 
typedef std::vector< smtrat::ConstraintT > ConstraintVector
 a vector of constraints More...
 
typedef std::vector< ConstraintVector > DisjunctionOfConstraintConjunctions
 a vector of vectors of constraints More...
 
template<typename T >
using SubstitutionFastPointerMap = std::unordered_map< const smtrat::Poly *, T, substitutionPointerHash, substitutionPointerEqual >
 

Functions

std::ostream & operator<< (std::ostream &_out, const Condition &_condition)
 
void simplify (DisjunctionOfConstraintConjunctions &)
 Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. More...
 
void simplify (DisjunctionOfConstraintConjunctions &_toSimplify, Variables &_conflictingVars, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
bool splitProducts (DisjunctionOfConstraintConjunctions &, 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...
 
bool splitProducts (const ConstraintVector &, DisjunctionOfConstraintConjunctions &, 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...
 
DisjunctionOfConstraintConjunctions splitProducts (const smtrat::ConstraintT &, bool=false)
 Splits the given constraint into a set of constraints which compare the factors of the factorization of the constraints considered polynomial. More...
 
void splitSosDecompositions (DisjunctionOfConstraintConjunctions &_toSimplify)
 
DisjunctionOfConstraintConjunctions getSignCombinations (const smtrat::ConstraintT &)
 For a given constraint f_1*...*f_n ~ 0 this method computes all combinations of constraints f_1 ~_1 0 ... More...
 
void getOddBitStrings (std::size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
 
void getEvenBitStrings (std::size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
 
void print (DisjunctionOfConstraintConjunctions &_substitutionResults)
 Prints the given disjunction of conjunction of constraints. More...
 
bool substitute (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
bool substituteNormal (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
bool substituteNormalSqrtEq (const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
 Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More...
 
bool substituteNormalSqrtNeq (const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
 Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More...
 
bool substituteNormalSqrtLess (const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, const smtrat::Poly &_s, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
 Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More...
 
bool substituteNormalSqrtLeq (const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, const smtrat::Poly &_s, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
 Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square root. More...
 
bool substitutePlusEps (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
bool substituteEpsGradients (const smtrat::ConstraintT &_cons, const Substitution &_subs, const Relation _relation, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
void substituteInf (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
 
void substituteInfLessGreater (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_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...
 
void substituteTrivialCase (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_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...
 
void substituteNotTrivialCase (const smtrat::ConstraintT &, const Substitution &, DisjunctionOfConstraintConjunctions &)
 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...
 
template<class combineType >
bool combine (const std::vector< std::vector< std::vector< combineType > > > &_toCombine, std::vector< std::vector< combineType > > &_combination)
 Combines vectors. More...
 
void simplify (DisjunctionOfConstraintConjunctions &, carl::Variables &, const smtrat::EvalDoubleIntervalMap &)
 Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. 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)
 
bool substitute (const smtrat::ConstraintT &, const Substitution &, DisjunctionOfConstraintConjunctions &, bool _accordingPaper, carl::Variables &, const smtrat::EvalDoubleIntervalMap &)
 Applies a substitution to a constraint and stores the results in the given vector. More...
 
bool substituteNormal (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, carl::Variables &_conflictingVariables, const smtrat::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...
 
bool substitutePlusEps (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, carl::Variables &_conflictingVariables, const smtrat::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...
 
bool substituteEpsGradients (const smtrat::ConstraintT &_cons, const Substitution &_subs, const carl::Relation _relation, DisjunctionOfConstraintConjunctions &, bool _accordingPaper, carl::Variables &_conflictingVariables, const smtrat::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...
 
void substituteInf (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, carl::Variables &_conflictingVariables, const smtrat::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...
 
std::ostream & operator<< (std::ostream &os, const Substitution &s)
 Prints the given substitution on the given output stream. More...
 

Typedef Documentation

◆ ConditionList

typedef std::list< const Condition* > smtrat::vs::ConditionList

Definition at line 30 of file State.h.

◆ ConditionSetSet

typedef std::set< carl::PointerSet<Condition> > smtrat::vs::ConditionSetSet

Definition at line 28 of file State.h.

◆ ConditionSetSetSet

typedef std::set< ConditionSetSet > smtrat::vs::ConditionSetSetSet

Definition at line 29 of file State.h.

◆ ConstraintVector

typedef std::vector<smtrat::ConstraintT> smtrat::vs::ConstraintVector

a vector of constraints

Definition at line 31 of file Substitute.h.

◆ DisjunctionOfConditionConjunctions

typedef std::vector< ConditionList > smtrat::vs::DisjunctionOfConditionConjunctions

Definition at line 31 of file State.h.

◆ DisjunctionOfConstraintConjunctions

typedef std::vector<ConstraintVector> smtrat::vs::DisjunctionOfConstraintConjunctions

a vector of vectors of constraints

Definition at line 33 of file Substitute.h.

◆ SubstitutionFastPointerMap

template<typename T >
using smtrat::vs::SubstitutionFastPointerMap = typedef std::unordered_map<const smtrat::Poly*, T, substitutionPointerHash, substitutionPointerEqual>

Definition at line 228 of file Substitution.h.

◆ UnsignedTriple

typedef std::pair<size_t, std::pair<size_t, size_t> > smtrat::vs::UnsignedTriple

Definition at line 33 of file State.h.

◆ ValStatePair

typedef std::pair<UnsignedTriple, vs::State*> smtrat::vs::ValStatePair

Definition at line 61 of file State.h.

◆ ValuationMap

typedef std::map<UnsignedTriple, vs::State*, unsignedTripleCmp> smtrat::vs::ValuationMap

Definition at line 62 of file State.h.

Function Documentation

◆ combine()

template<class combineType >
bool smtrat::vs::combine ( const std::vector< std::vector< std::vector< combineType > > > &  _toCombine,
std::vector< std::vector< combineType > > &  _combination 
)

Combines vectors.

Parameters
_toCombineThe vectors to combine.
_combinationThe 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.

Definition at line 44 of file Substitute.h.

Here is the caller graph for this function:

◆ getEvenBitStrings() [1/2]

void smtrat::vs::getEvenBitStrings ( size_t  _length,
std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &  _strings 
)
Parameters
_lengthThe maximal length of the bit strings with even parity to compute.
_stringsAll bit strings of length less or equal the given length with even parity.

◆ getEvenBitStrings() [2/2]

void smtrat::vs::getEvenBitStrings ( std::size_t  _length,
std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &  _strings 
)

Definition at line 512 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getOddBitStrings() [1/2]

void smtrat::vs::getOddBitStrings ( size_t  _length,
std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &  _strings 
)
Parameters
_lengthThe maximal length of the bit strings with odd parity to compute.
_stringsAll bit strings of length less or equal the given length with odd parity.

◆ getOddBitStrings() [2/2]

void smtrat::vs::getOddBitStrings ( std::size_t  _length,
std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &  _strings 
)

Definition at line 494 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getSignCombinations()

DisjunctionOfConstraintConjunctions smtrat::vs::getSignCombinations ( const smtrat::ConstraintT &  )

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
_constraintA pointer to the constraint to split this way.
Returns
The resulting combinations.

Definition at line 397 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ operator<<() [1/2]

std::ostream& smtrat::vs::operator<< ( std::ostream &  _out,
const Condition &  _condition 
)

Definition at line 246 of file Condition.cpp.

◆ operator<<() [2/2]

std::ostream & smtrat::vs::operator<< ( std::ostream &  os,
const Substitution &  s 
)

Prints the given substitution on the given output stream.

Parameters
_outThe output stream, on which to write.
_substitutionThe substitution to print.
Returns
The output stream after printing the substitution on it.

Definition at line 164 of file Substitution.cpp.

Here is the call graph for this function:

◆ print()

void smtrat::vs::print ( DisjunctionOfConstraintConjunctions &  _substitutionResults)

Prints the given disjunction of conjunction of constraints.

Parameters
_substitutionResultsThe disjunction of conjunction of constraints to print.

Definition at line 530 of file Substitute.cpp.

Here is the caller graph for this function:

◆ simplify() [1/3]

void smtrat::vs::simplify ( DisjunctionOfConstraintConjunctions &  )

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
_toSimplifyThe disjunction of conjunctions to simplify.

Definition at line 25 of file Substitute.cpp.

◆ simplify() [2/3]

void smtrat::vs::simplify ( DisjunctionOfConstraintConjunctions &  ,
carl::Variables &  ,
const smtrat::EvalDoubleIntervalMap &   
)

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
_toSimplifyThe disjunction of conjunctions to simplify.
_conflictingVars
_solutionSpace

◆ simplify() [3/3]

void smtrat::vs::simplify ( DisjunctionOfConstraintConjunctions &  _toSimplify,
Variables &  _conflictingVars,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 59 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ splitProducts() [1/3]

bool smtrat::vs::splitProducts ( const ConstraintVector &  ,
DisjunctionOfConstraintConjunctions &  ,
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.

Parameters
_toSimplifyThe conjunction of the constraints to split.
_resultThe result, being a disjunction of conjunctions of constraints.
_onlyNeqA 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.

Definition at line 135 of file Substitute.cpp.

Here is the call graph for this function:

◆ splitProducts() [2/3]

DisjunctionOfConstraintConjunctions smtrat::vs::splitProducts ( const smtrat::ConstraintT &  ,
bool  = false 
)

Splits the given constraint into a set of constraints which compare the factors of the factorization of the constraints considered polynomial.

Parameters
_constraintA pointer to the constraint to split.
_onlyNeqA 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.

Definition at line 204 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ splitProducts() [3/3]

bool smtrat::vs::splitProducts ( DisjunctionOfConstraintConjunctions &  ,
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.

Parameters
_toSimplifyThe disjunction of conjunctions of the constraints to split.
_onlyNeqA 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.

Definition at line 114 of file Substitute.cpp.

Here is the call graph for this function:

◆ splitSosDecompositions()

void smtrat::vs::splitSosDecompositions ( DisjunctionOfConstraintConjunctions &  _toSimplify)

Definition at line 262 of file Substitute.cpp.

Here is the caller graph for this function:

◆ substitute() [1/2]

bool smtrat::vs::substitute ( const smtrat::ConstraintT &  ,
const Substitution &  ,
DisjunctionOfConstraintConjunctions &  ,
bool  _accordingPaper,
carl::Variables &  ,
const smtrat::EvalDoubleIntervalMap &   
)

Applies a substitution to a constraint and stores the results in the given vector.

Parameters
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe 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.

◆ substitute() [2/2]

bool smtrat::vs::substitute ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
Variables &  _conflictingVariables,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 553 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteEpsGradients() [1/2]

bool smtrat::vs::substituteEpsGradients ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
const carl::Relation  _relation,
DisjunctionOfConstraintConjunctions &  ,
bool  _accordingPaper,
carl::Variables &  _conflictingVariables,
const smtrat::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.

Parameters
_consThe constraint to substitute in.
_subsThe substitution to apply.
_relationThe relation symbol, deciding whether the substitution result must be negative or positive.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).
_conflictingVariablesIf a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container.
_solutionSpaceThe solution space in form of double intervals of the variables occurring in the given constraint.

◆ substituteEpsGradients() [2/2]

bool smtrat::vs::substituteEpsGradients ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
const Relation  _relation,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
Variables &  _conflictingVariables,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 991 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteInf() [1/2]

void smtrat::vs::substituteInf ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
carl::Variables &  _conflictingVariables,
const smtrat::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.

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
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_conflictingVariablesIf a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container.
_solutionSpaceThe solution space in form of double intervals of the variables occurring in the given constraint.

◆ substituteInf() [2/2]

void smtrat::vs::substituteInf ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
Variables &  _conflictingVariables,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 1041 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteInfLessGreater()

void smtrat::vs::substituteInfLessGreater ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _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.

The constraint is of the form "a*x^2+bx+c \rho 0", where \rho is less or greater.

Parameters
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.

Definition at line 1066 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteNormal() [1/2]

bool smtrat::vs::substituteNormal ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
carl::Variables &  _conflictingVariables,
const smtrat::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.

Parameters
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).
_conflictingVariablesIf a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container.
_solutionSpaceThe solution space in form of double intervals of the variables occurring in the given constraint.

◆ substituteNormal() [2/2]

bool smtrat::vs::substituteNormal ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
Variables &  _conflictingVariables,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 608 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteNormalSqrtEq()

bool smtrat::vs::substituteNormalSqrtEq ( const smtrat::Poly &  _radicand,
const smtrat::Poly &  _q,
const smtrat::Poly &  _r,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper 
)

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
_radicandThe radicand of the square root.
_qThe summand not containing the square root.
_rThe coefficient of the radicand.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).

Definition at line 731 of file Substitute.cpp.

Here is the caller graph for this function:

◆ substituteNormalSqrtLeq()

bool smtrat::vs::substituteNormalSqrtLeq ( const smtrat::Poly &  _radicand,
const smtrat::Poly &  _q,
const smtrat::Poly &  _r,
const smtrat::Poly &  _s,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper 
)

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
_radicandThe radicand of the square root.
_qThe summand not containing the square root.
_rThe coefficient of the radicand.
_sThe denominator of the expression containing the square root.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).

Definition at line 869 of file Substitute.cpp.

Here is the caller graph for this function:

◆ substituteNormalSqrtLess()

bool smtrat::vs::substituteNormalSqrtLess ( const smtrat::Poly &  _radicand,
const smtrat::Poly &  _q,
const smtrat::Poly &  _r,
const smtrat::Poly &  _s,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper 
)

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
_radicandThe radicand of the square root.
_qThe summand not containing the square root.
_rThe coefficient of the radicand.
_sThe denominator of the expression containing the square root.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).

Definition at line 806 of file Substitute.cpp.

Here is the caller graph for this function:

◆ substituteNormalSqrtNeq()

bool smtrat::vs::substituteNormalSqrtNeq ( const smtrat::Poly &  _radicand,
const smtrat::Poly &  _q,
const smtrat::Poly &  _r,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper 
)

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
_radicandThe radicand of the square root.
_qThe summand not containing the square root.
_rThe coefficient of the radicand.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).

Definition at line 772 of file Substitute.cpp.

Here is the caller graph for this function:

◆ substituteNotTrivialCase()

void smtrat::vs::substituteNotTrivialCase ( const smtrat::ConstraintT &  ,
const Substitution &  ,
DisjunctionOfConstraintConjunctions &   
)

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
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.

Definition at line 1121 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substitutePlusEps() [1/2]

bool smtrat::vs::substitutePlusEps ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
carl::Variables &  _conflictingVariables,
const smtrat::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.

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
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.
_accordingPaperA 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).
_conflictingVariablesIf a conflict with the given solution space occurs, the variables being part of this conflict are stored in this container.
_solutionSpaceThe solution space in form of double intervals of the variables occurring in the given constraint.

◆ substitutePlusEps() [2/2]

bool smtrat::vs::substitutePlusEps ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result,
bool  _accordingPaper,
Variables &  _conflictingVariables,
const smtrat::EvalDoubleIntervalMap &  _solutionSpace 
)

Definition at line 926 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ substituteTrivialCase()

void smtrat::vs::substituteTrivialCase ( const smtrat::ConstraintT &  _cons,
const Substitution &  _subs,
DisjunctionOfConstraintConjunctions &  _result 
)

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
_consThe constraint to substitute in.
_subsThe substitution to apply.
_resultThe vector, in which to store the results of this substitution. It is semantically a disjunction of conjunctions of constraints.

Definition at line 1111 of file Substitute.cpp.

Here is the call graph for this function:
Here is the caller graph for this function: