substitute.h File Reference
#include <bitset>#include <vector>#include <carl-formula/arithmetic/Constraint.h>#include "term.h"#include "zeros.h"#include "substitute.tpp"
Include dependency graph for substitute.h:
Go to the source code of this file.
Data Structures | |
| struct | carl::vs::detail::Substitution< Poly > |
Namespaces | |
| carl | |
| carl is the main namespace for the library. | |
| carl::vs | |
| carl::vs::detail | |
Typedefs | |
| template<typename Poly > | |
| using | carl::vs::ConstraintConjunction = std::vector< Constraint< Poly > > |
| a vector of constraints More... | |
| template<typename Poly > | |
| using | carl::vs::CaseDistinction = std::vector< ConstraintConjunction< Poly > > |
| a vector of vectors of constraints More... | |
| using | carl::vs::detail::DoubleInterval = carl::Interval< double > |
| using | carl::vs::detail::EvalDoubleIntervalMap = std::map< carl::Variable, DoubleInterval > |
Functions | |
| template<class Poly > | |
| std::ostream & | carl::vs::detail::operator<< (std::ostream &os, const Substitution< Poly > &s) |
| template<class combineType > | |
| bool | carl::vs::detail::combine (const std::vector< std::vector< std::vector< combineType > > > &_toCombine, std::vector< std::vector< combineType > > &_combination) |
| Combines vectors. More... | |
| template<typename Poly > | |
| void | carl::vs::detail::simplify (CaseDistinction< Poly > &) |
| Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. More... | |
| template<typename Poly > | |
| void | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 > | carl::vs::detail::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 | carl::vs::detail::splitSosDecompositions (CaseDistinction< Poly > &) |
| template<typename Poly > | |
| CaseDistinction< Poly > | carl::vs::detail::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 | carl::vs::detail::getOddBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings) |
| void | carl::vs::detail::getEvenBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings) |
| template<typename Poly > | |
| void | carl::vs::detail::print (CaseDistinction< Poly > &_substitutionResults) |
| Prints the given disjunction of conjunction of constraints. More... | |
| template<typename Poly > | |
| bool | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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 | carl::vs::detail::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... | |
| template<typename Poly > | |
| bool | carl::vs::simplify_inplace (CaseDistinction< Poly > &cases) |
| Simplifies the case distinction in place. More... | |
| template<typename Poly > | |
| std::optional< CaseDistinction< Poly > > | carl::vs::substitute (const Constraint< Poly > &cons, const Variable var, const Term< Poly > &term) |
| Applies a substitution to a constraint. More... | |
| template<typename Poly > | |
| static std::optional< std::variant< CaseDistinction< Poly >, VariableComparison< Poly > > > | carl::vs::substitute (const VariableComparison< Poly > &varcomp, const Variable var, const Term< Poly > &term) |
| Applies a substitution to a variable comparison. More... | |
Variables | |
| const unsigned | MAX_PRODUCT_SPLIT_NUMBER = 64 |
| The maximal number of splits performed, if the left-hand side of a constraints is a product of polynomials and we split the constraint into constraints over these polynomials according to the relation. More... | |
| const unsigned | MAX_NUM_OF_COMBINATION_RESULT = 1025 |
| The maximum number of the resulting combinations when combining according to the method combine. More... | |
Variable Documentation
◆ MAX_NUM_OF_COMBINATION_RESULT
| const unsigned MAX_NUM_OF_COMBINATION_RESULT = 1025 |
The maximum number of the resulting combinations when combining according to the method combine.
If this number is exceeded, the method return false, and no combining is performed.
Definition at line 21 of file substitute.h.
◆ MAX_PRODUCT_SPLIT_NUMBER
| const unsigned MAX_PRODUCT_SPLIT_NUMBER = 64 |
The maximal number of splits performed, if the left-hand side of a constraints is a product of polynomials and we split the constraint into constraints over these polynomials according to the relation.
Definition at line 16 of file substitute.h.
