VSHelper.h File Reference

#include <smtrat-common/smtrat-common.h>
#include <smtrat-common/model.h>
#include <carl-arith/core/Common.h>
#include <carl-formula/model/evaluation/ModelEvaluation.h>
#include <carl-vs/substitute.h>
#include <carl-vs/zeros.h>
#include <variant>
#include <vector>

Include dependency graph for VSHelper.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::mcsat::vs::helper::TestCandidate

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

Functions
void	smtrat::mcsat::vs::helper::getFormulaAtoms (const FormulaT &f, FormulaSetT &result)
FormulaT	smtrat::mcsat::vs::helper::to_formula (const carl::vs::CaseDistinction< Poly > &docc)
	Converts a DisjunctionOfConstraintConjunctions to a regular Formula. More...
static bool	smtrat::mcsat::vs::helper::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	smtrat::mcsat::vs::helper::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	smtrat::mcsat::vs::helper::generateTestCandidates (std::vector< TestCandidate > &results, const carl::Variable &eliminationVar, const FormulaSetT &constraints)
	Generate all test candidates according to "vanilla" virtual substitution. More...
bool	smtrat::mcsat::vs::helper::substitute (const FormulaT &constr, const carl::Variable var, const carl::vs::Term< Poly > &term, FormulaT &result)