Substitute.cpp File Reference

#include "Substitute.h"
#include <cmath>
#include <limits>
#include <carl-arith/poly/umvpoly/functions/Derivative.h>
#include <carl-arith/poly/umvpoly/functions/SoSDecomposition.h>
#include <carl-arith/constraint/IntervalEvaluation.h>
#include <carl-arith/vs/Substitution.h>

Include dependency graph for Substitute.cpp:

Go to the source code of this file.

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

Functions
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 &_toSimplify, Variables &_conflictingVars, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
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 (std::size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
void	smtrat::vs::getEvenBitStrings (std::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 &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
bool	smtrat::vs::substituteNormal (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
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, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
bool	smtrat::vs::substituteEpsGradients (const smtrat::ConstraintT &_cons, const Substitution &_subs, const Relation _relation, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
void	smtrat::vs::substituteInf (const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
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_NUM_OF_TERMS = 512
	Class containing a method applying a virtual substitution. More...

Variable Documentation

MAX_NUM_OF_TERMS

const unsigned MAX_NUM_OF_TERMS = 512

Class containing a method applying a virtual substitution.

Author

Florian Corzilius

Since

2011-05-23

Version

2013-10-23

Definition at line 18 of file Substitute.cpp.