Substitute.h File Reference

#include <smtrat-common/smtrat-common.h>
#include "Substitution.h"
#include <bitset>

Include dependency graph for Substitute.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::vs

Typedefs
typedef std::vector< smtrat::ConstraintT >	smtrat::vs::ConstraintVector
	a vector of constraints More...
typedef std::vector< ConstraintVector >	smtrat::vs::DisjunctionOfConstraintConjunctions
	a vector of vectors of constraints More...

Functions
template<class combineType >
bool	smtrat::vs::combine (const std::vector< std::vector< std::vector< combineType > > > &_toCombine, std::vector< std::vector< combineType > > &_combination)
	Combines vectors. More...
void	smtrat::vs::simplify (DisjunctionOfConstraintConjunctions &)
	Simplifies a disjunction of conjunctions of constraints by deleting consistent constraint and inconsistent conjunctions of constraints. More...
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. More...
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. More...
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. More...
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. More...
void	smtrat::vs::splitSosDecompositions (DisjunctionOfConstraintConjunctions &_toSimplify)
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 ... More...
void	smtrat::vs::getOddBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
void	smtrat::vs::getEvenBitStrings (size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
void	smtrat::vs::print (DisjunctionOfConstraintConjunctions &_substitutionResults)
	Prints the given disjunction of conjunction of constraints. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...
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. More...

Variables
const unsigned	MAX_PRODUCT_SPLIT_NUMBER = 64
	Class containing a method applying a virtual substitution. 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 24 of file Substitute.h.

MAX_PRODUCT_SPLIT_NUMBER

const unsigned MAX_PRODUCT_SPLIT_NUMBER = 64

Class containing a method applying a virtual substitution.

Author

Florian Corzilius

Since

2011-05-23

Version

2013-10-23 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 19 of file Substitute.h.