smtrat::subtropical::Encoding Class Reference

#include <Subtropical.h>

Collaboration diagram for smtrat::subtropical::Encoding:

Public Member Functions
FormulaT	encode_separator (const Separator &separator, const Direction direction, const SeparatorType separator_type)
	Creates the formula for the hyperplane that linearly separates at least one variant positive frame vertex from all variant negative frame vertices. More...
FormulaT	encode_integer (carl::Variable var)
Model	construct_assignment (const Model &lra_model, const FormulaT &f) const

Private Attributes
std::unordered_map< carl::Variable, Moment >	m_moments
	Maps a variable to the components of the moment function. More...

Detailed Description

Definition at line 106 of file Subtropical.h.

Member Function Documentation

construct_assignment()

Model smtrat::subtropical::Encoding::construct_assignment ( const Model &  lra_model, const FormulaT &  f  ) const

inline

Stores all informations retrieved from the LRA solver to construct the model

Definition at line 195 of file Subtropical.h.

Here is the call graph for this function:

encode_integer()

FormulaT smtrat::subtropical::Encoding::encode_integer ( carl::Variable  var )

inline

Definition at line 190 of file Subtropical.h.

Here is the call graph for this function:

encode_separator()

FormulaT smtrat::subtropical::Encoding::encode_separator ( const Separator &  separator, const Direction  direction, const SeparatorType  separator_type  )

inline

Creates the formula for the hyperplane that linearly separates at least one variant positive frame vertex from all variant negative frame vertices.

If a weak separator is searched, the corresponding rating is included.

Parameters

separator	The separator object that stores the construction information.
negated	True, if the formula for the negated polynomial shall be constructed. False, if the formula for the original polynomial shall be constructed.

Returns

Formula that is satisfiable iff such a separating hyperplane exists.

Create the hyperplane and sign change formula

Create the rating case distinction formula

Create the strict/weak linear separating hyperplane

Definition at line 120 of file Subtropical.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

m_moments

std::unordered_map<carl::Variable, Moment> smtrat::subtropical::Encoding::m_moments

private

Maps a variable to the components of the moment function.

Definition at line 108 of file Subtropical.h.

---

The documentation for this class was generated from the following file:

• smtrat-modules/STropModule/Subtropical.h