utils.h File Reference

#include <carl-arith/poly/umvpoly/functions/Substitution.h>
#include <carl-formula/model/evaluation/ModelEvaluation.h>
#include <smtrat-common/model.h>
#include <smtrat-common/smtrat-common.h>

Include dependency graph for utils.h:

Go to the source code of this file.

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

Functions
Rational	smtrat::lve::evaluate (carl::Variable v, const Poly &p, const Rational &r)
carl::Sign	smtrat::lve::sgn (carl::Variable v, const Poly &p, const RAN &r)
std::optional< ModelValue >	smtrat::lve::get_root (carl::Variable v, const Poly &p)
ModelValue	smtrat::lve::get_non_root (carl::Variable v, const Poly &p)
std::optional< ModelValue >	smtrat::lve::get_value_for_sgn (carl::Variable v, const Poly &p, carl::Sign sign)
carl::Sign	smtrat::lve::sgn_of_invariant_poly (carl::Variable v, const Poly &p)