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

Take conjunctions incrementally, construct linear formulas for LRA solver. More...

#include <STropSettings.h>

Static Public Attributes

static constexpr auto moduleName = "STropModule<STropSettings1>"
 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::INCREMENTAL_CONSTRAINTS
 incremental mode for SMT solving More...
 
static constexpr bool output_only = false
 

Detailed Description

Take conjunctions incrementally, construct linear formulas for LRA solver.

Definition at line 19 of file STropSettings.h.

Field Documentation

◆ mode

constexpr Mode smtrat::STropSettings1::mode = Mode::INCREMENTAL_CONSTRAINTS
staticconstexpr

incremental mode for SMT solving

Definition at line 25 of file STropSettings.h.

◆ moduleName

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

Name of the Module.

Definition at line 21 of file STropSettings.h.

◆ output_only

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

Definition at line 27 of file STropSettings.h.

◆ separatorType

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

Type of linear separating hyperplane to search for.

Definition at line 23 of file STropSettings.h.

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