Subtropical.h File Reference

#include <carl-arith/constraint/BasicConstraint.h>
#include <boost/container/flat_map.hpp>

Include dependency graph for Subtropical.h:

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

Go to the source code of this file.

Data Structures
struct	smtrat::subtropical::Moment
	Represents the normal vector component and the sign variable assigned to a variable in an original constraint. More...
struct	smtrat::subtropical::Vertex
	Represents a term of an original constraint and assigns him a rating variable if a weak separator is searched. More...
struct	smtrat::subtropical::Separator
	Represents the class of all original constraints with the same left hand side after a normalization. More...
class	smtrat::subtropical::Encoding

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::subtropical
	Implements data structures and encodings for the subtropical method.

Enumerations
enum class	smtrat::subtropical::SeparatorType { smtrat::subtropical::STRICT = 0 , smtrat::subtropical::WEAK = 1 , smtrat::subtropical::SEMIWEAK = 2 }
enum class	smtrat::subtropical::Direction { smtrat::subtropical::BOTH = 0 , smtrat::subtropical::NEGATIVE = 1 , smtrat::subtropical::POSITIVE = 2 }
	Subdivides the relations into classes with the same linearization result. More...

Functions
carl::BasicConstraint< Poly >	smtrat::subtropical::normalize (const carl::BasicConstraint< Poly > &c)
std::optional< Direction >	smtrat::subtropical::direction (carl::Relation r)
std::optional< Direction >	smtrat::subtropical::direction_for_equality (const Separator &s)
FormulaT	smtrat::subtropical::transform_to_equation (const FormulaT &formula)
	Requires a quantifier-free real arithmetic formula with no negations. More...
FormulaT	smtrat::subtropical::encode_as_formula (const FormulaT &formula, Encoding &encoding, SeparatorType separator_type)
	Requires a quantifier-free real arithmetic formula with no negations. More...
FormulaT	smtrat::subtropical::encode_as_formula_alt (const FormulaT &formula, Encoding &encoding, SeparatorType separator_type)
	Requires a quantifier-free real arithmetic formula with no negations. More...