SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Static Public Attributes
smtrat::STropSettings3 Struct Reference

Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve. More...

#include <STropSettings.h>

Static Public Attributes

static constexpr auto moduleName = "STropModule<STropSettings3>"
 Name of the Module. More...
 
static constexpr subtropical::SeparatorType separatorType = subtropical::SeparatorType::SEMIWEAK
 Type of linear separating hyperplane to search for. More...
 
static constexpr Mode mode = Mode::TRANSFORM_FORMULA
 transformation of the formula to a linear formula, preserving the Boolean structure More...
 
static constexpr bool output_only = false
 

Detailed Description

Transform to NNF then replace each constraint with its linear formula (equations become FALSE). Then let LRA solver solve.

Definition at line 47 of file STropSettings.h.

Field Documentation

◆ mode

constexpr Mode smtrat::STropSettings3::mode = Mode::TRANSFORM_FORMULA
staticconstexpr

transformation of the formula to a linear formula, preserving the Boolean structure

Definition at line 53 of file STropSettings.h.

◆ moduleName

constexpr auto smtrat::STropSettings3::moduleName = "STropModule<STropSettings3>"
staticconstexpr

Name of the Module.

Definition at line 49 of file STropSettings.h.

◆ output_only

constexpr bool smtrat::STropSettings3::output_only = false
staticconstexpr

Definition at line 55 of file STropSettings.h.

◆ separatorType

constexpr subtropical::SeparatorType smtrat::STropSettings3::separatorType = subtropical::SeparatorType::SEMIWEAK
staticconstexpr

Type of linear separating hyperplane to search for.

Definition at line 51 of file STropSettings.h.

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