smtrat::subtropical Namespace Reference

Implements data structures and encodings for the subtropical method. More...

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

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

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

Detailed Description

Implements data structures and encodings for the subtropical method.

Enumeration Type Documentation

Direction

enum smtrat::subtropical::Direction

strong

Subdivides the relations into classes with the same linearization result.

Enumerator
BOTH
NEGATIVE
POSITIVE

Definition at line 53 of file Subtropical.h.

SeparatorType

enum smtrat::subtropical::SeparatorType

strong

Enumerator
STRICT
WEAK
SEMIWEAK

Definition at line 13 of file Subtropical.h.

Function Documentation

direction()

std::optional<Direction> smtrat::subtropical::direction ( carl::Relation  r )

inline

Definition at line 62 of file Subtropical.h.

Here is the caller graph for this function:

direction_for_equality()

std::optional<Direction> smtrat::subtropical::direction_for_equality ( const Separator &  s )

inline

Definition at line 96 of file Subtropical.h.

encode_as_formula()

FormulaT smtrat::subtropical::encode_as_formula ( const FormulaT &  formula, Encoding &  encoding, SeparatorType  separator_type  )

inline

Requires a quantifier-free real arithmetic formula with no negations.

Parameters

formula

The formula to translate

Returns

linear formula

Definition at line 319 of file Subtropical.h.

Here is the call graph for this function:

encode_as_formula_alt()

FormulaT smtrat::subtropical::encode_as_formula_alt ( const FormulaT &  formula, Encoding &  encoding, SeparatorType  separator_type  )

inline

Requires a quantifier-free real arithmetic formula with no negations.

Parameters

formula

The formula to translate

Returns

linear formula

Definition at line 360 of file Subtropical.h.

Here is the call graph for this function:

normalize()

carl::BasicConstraint<Poly> smtrat::subtropical::normalize ( const carl::BasicConstraint< Poly > &  c )

inline

Definition at line 57 of file Subtropical.h.

Here is the caller graph for this function:

transform_to_equation()

FormulaT smtrat::subtropical::transform_to_equation ( const FormulaT &  formula )

inline

Requires a quantifier-free real arithmetic formula with no negations.

Parameters

formula

The formula to transform

Returns

an equisatisfiable equation

Definition at line 258 of file Subtropical.h.

Here is the call graph for this function: