smtrat::mcsat::vs::helper Namespace Reference

Data Structures
struct	TestCandidate

Functions
void	getFormulaAtoms (const FormulaT &f, FormulaSetT &result)
FormulaT	to_formula (const carl::vs::CaseDistinction< Poly > &docc)
	Converts a DisjunctionOfConstraintConjunctions to a regular Formula. More...
static bool	generateZeros (const FormulaT &formula, const carl::Variable &eliminationVar, std::function< void(SqrtEx &&sqrtExpression, ConstraintsT &&sideConditions)> yield_result)
	Get zeros with side conditions of the given constraint. More...
static bool	addOrMergeTestCandidate (std::vector< TestCandidate > &results, const TestCandidate &newSubstitution)
	Adds a new substitution to the given list of substitutions or merges it to an existing one. More...
static bool	generateTestCandidates (std::vector< TestCandidate > &results, const carl::Variable &eliminationVar, const FormulaSetT &constraints)
	Generate all test candidates according to "vanilla" virtual substitution. More...
bool	substitute (const FormulaT &constr, const carl::Variable var, const carl::vs::Term< Poly > &term, FormulaT &result)

Function Documentation

addOrMergeTestCandidate()

static bool smtrat::mcsat::vs::helper::addOrMergeTestCandidate ( std::vector< TestCandidate > &  results, const TestCandidate &  newSubstitution  )

static

Adds a new substitution to the given list of substitutions or merges it to an existing one.

Returns true if a new substitution was created.

Definition at line 93 of file VSHelper.h.

Here is the call graph for this function:

Here is the caller graph for this function:

generateTestCandidates()

static bool smtrat::mcsat::vs::helper::generateTestCandidates ( std::vector< TestCandidate > &  results, const carl::Variable &  eliminationVar, const FormulaSetT &  constraints  )

static

Generate all test candidates according to "vanilla" virtual substitution.

Returns false iff VS is not applicable.

Definition at line 105 of file VSHelper.h.

Here is the call graph for this function:

Here is the caller graph for this function:

generateZeros()

static bool smtrat::mcsat::vs::helper::generateZeros ( const FormulaT &  formula, const carl::Variable &  eliminationVar, std::function< void(SqrtEx &&sqrtExpression, ConstraintsT &&sideConditions)>  yield_result  )

static

Get zeros with side conditions of the given constraint.

Kind of a generator function. Passes generated zeros to a callback function to avoid copying.

Definition at line 54 of file VSHelper.h.

Here is the caller graph for this function:

getFormulaAtoms()

void smtrat::mcsat::vs::helper::getFormulaAtoms ( const FormulaT &  f, FormulaSetT &  result  )

inline

Definition at line 18 of file VSHelper.h.

Here is the caller graph for this function:

substitute()

bool smtrat::mcsat::vs::helper::substitute ( const FormulaT &  constr, const carl::Variable  var, const carl::vs::Term< Poly > &  term, FormulaT &  result  )

inline

Definition at line 138 of file VSHelper.h.

Here is the call graph for this function:

Here is the caller graph for this function:

to_formula()

FormulaT smtrat::mcsat::vs::helper::to_formula ( const carl::vs::CaseDistinction< Poly > &  docc )

inline

Converts a DisjunctionOfConstraintConjunctions to a regular Formula.

Definition at line 37 of file VSHelper.h.

Here is the caller graph for this function: