to_formula.cpp File Reference

#include "to_formula.h"
#include "smtrat-cadcells/datastructures/roots.h"
#include "smtrat-common/types.h"
#include <carl-arith/extended/MultivariateRoot.h>
#include <carl-arith/poly/Conversion.h>
#include <carl-arith/constraint/Conversion.h>
#include <carl-arith/extended/Conversion.h>
#include <smtrat-cadcells/common.h>
#include <smtrat-coveringng/types.h>
#include <smtrat-cadcells/helper_formula.h>
#include <carl-formula/formula/functions/NNF.h>

Include dependency graph for to_formula.cpp:

Go to the source code of this file.

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::qe
	smtrat::qe::coverings
	smtrat::qe::coverings::util

Functions
FormulaT	smtrat::qe::coverings::util::to_formula (const cadcells::datastructures::PolyPool &pool, carl::Variable variable, const cadcells::datastructures::SymbolicInterval &interval)
FormulaT	smtrat::qe::coverings::util::to_formula_true_only (const cadcells::datastructures::PolyPool &pool, const covering_ng::ParameterTree &tree)
FormulaT	smtrat::qe::coverings::util::to_formula_alternate (const cadcells::datastructures::PolyPool &pool, const covering_ng::ParameterTree &tree, bool positive)
FormulaT	smtrat::qe::coverings::util::to_formula_alternate (const cadcells::datastructures::PolyPool &pool, const covering_ng::ParameterTree &tree)