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

#include <LRASettings.h>

Inheritance diagram for smtrat::LRASettings1::Tableau_settings:
Inheritance graph
[legend]
Collaboration diagram for smtrat::LRASettings1::Tableau_settings:
Collaboration graph
[legend]

Static Public Attributes

static const bool use_pivoting_strategy = true
 
static const bool use_refinement = true
 
static const bool prefer_equations = false
 
static const bool pivot_into_local_conflict = true
 
static const bool use_activity_based_pivot_strategy = false
 
static const bool use_theta_based_pivot_strategy = false
 
static const bool introduce_new_constraint_in_refinement = false
 
static const bool omit_division = true
 
static constexpr NBCS nonbasic_var_choice_strategy = NBCS::LESS_COLUMN_ENTRIES
 

Detailed Description

Definition at line 54 of file LRASettings.h.

Field Documentation

◆ introduce_new_constraint_in_refinement

const bool smtrat::lra::TableauSettings1::introduce_new_constraint_in_refinement = false
staticinherited

Definition at line 47 of file TableauSettings.h.

◆ nonbasic_var_choice_strategy

constexpr NBCS smtrat::lra::TableauSettings1::nonbasic_var_choice_strategy = NBCS::LESS_COLUMN_ENTRIES
staticconstexprinherited

Definition at line 55 of file TableauSettings.h.

◆ omit_division

const bool smtrat::lra::TableauSettings1::omit_division = true
staticinherited

Definition at line 51 of file TableauSettings.h.

◆ pivot_into_local_conflict

const bool smtrat::lra::TableauSettings1::pivot_into_local_conflict = true
staticinherited

Definition at line 35 of file TableauSettings.h.

◆ prefer_equations

const bool smtrat::lra::TableauSettings1::prefer_equations = false
staticinherited

Definition at line 31 of file TableauSettings.h.

◆ use_activity_based_pivot_strategy

const bool smtrat::lra::TableauSettings1::use_activity_based_pivot_strategy = false
staticinherited

Definition at line 39 of file TableauSettings.h.

◆ use_pivoting_strategy

const bool smtrat::lra::TableauSettings1::use_pivoting_strategy = true
staticinherited

Definition at line 23 of file TableauSettings.h.

◆ use_refinement

const bool smtrat::lra::TableauSettings1::use_refinement = true
staticinherited

Definition at line 27 of file TableauSettings.h.

◆ use_theta_based_pivot_strategy

const bool smtrat::lra::TableauSettings1::use_theta_based_pivot_strategy = false
staticinherited

Definition at line 43 of file TableauSettings.h.

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