SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Static Public Attributes
smtrat::STropSettings3b 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<STropSettings3b>"
 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_ALT
 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 59 of file STropSettings.h.

Field Documentation

◆ mode

constexpr Mode smtrat::STropSettings3b::mode = Mode::TRANSFORM_FORMULA_ALT
staticconstexpr

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

Definition at line 65 of file STropSettings.h.

◆ moduleName

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

Name of the Module.

Definition at line 61 of file STropSettings.h.

◆ output_only

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

Definition at line 67 of file STropSettings.h.

◆ separatorType

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

Type of linear separating hyperplane to search for.

Definition at line 63 of file STropSettings.h.

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