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

#include <VSSettings.h>

Inheritance diagram for smtrat::VSSettings1:
Inheritance graph
[legend]

Static Public Attributes

static constexpr auto moduleName = "VSModule<VSSettings1>"
 
static const bool elimination_with_factorization = false
 
static const bool local_conflict_search = false
 
static const bool use_backjumping = true
 
static const bool use_strict_inequalities_for_test_candidate_generation = true
 
static const bool use_variable_bounds = true
 
static const bool sturm_sequence_for_root_check = use_variable_bounds && false
 
static const bool check_conflict_for_side_conditions = false
 
static const bool incremental_solving = true
 
static const bool infeasible_subset_generation = true
 
static const bool virtual_substitution_according_paper = false
 
static const bool prefer_equation_over_all = false
 
static const bool mixed_int_real_constraints_allowed = false
 
static const bool split_neq_constraints = false
 
static const size_t int_max_range = 1
 
static const size_t lazy_check_threshold = 1
 
static const bool try_first_lazy = false
 
static const bool use_branch_and_bound = true
 
static const bool only_split_in_final_call = true
 
static const bool branch_and_bound_at_origin = false
 
static const bool use_fixed_variable_order = false
 
static constexpr auto variable_valuation_strategy = VariableValuationStrategy::OPTIMIZE_BEST
 
static constexpr bool make_constraints_strict_for_backend = true
 

Detailed Description

Definition at line 16 of file VSSettings.h.

Field Documentation

◆ branch_and_bound_at_origin

const bool smtrat::VSSettings1::branch_and_bound_at_origin = false
static

Definition at line 38 of file VSSettings.h.

◆ check_conflict_for_side_conditions

const bool smtrat::VSSettings1::check_conflict_for_side_conditions = false
static

Definition at line 26 of file VSSettings.h.

◆ elimination_with_factorization

const bool smtrat::VSSettings1::elimination_with_factorization = false
static

Definition at line 19 of file VSSettings.h.

◆ incremental_solving

const bool smtrat::VSSettings1::incremental_solving = true
static

Definition at line 27 of file VSSettings.h.

◆ infeasible_subset_generation

const bool smtrat::VSSettings1::infeasible_subset_generation = true
static

Definition at line 28 of file VSSettings.h.

◆ int_max_range

const size_t smtrat::VSSettings1::int_max_range = 1
static

Definition at line 33 of file VSSettings.h.

◆ lazy_check_threshold

const size_t smtrat::VSSettings1::lazy_check_threshold = 1
static

Definition at line 34 of file VSSettings.h.

◆ local_conflict_search

const bool smtrat::VSSettings1::local_conflict_search = false
static

Definition at line 20 of file VSSettings.h.

◆ make_constraints_strict_for_backend

constexpr bool smtrat::VSSettings1::make_constraints_strict_for_backend = true
staticconstexpr

Definition at line 42 of file VSSettings.h.

◆ mixed_int_real_constraints_allowed

const bool smtrat::VSSettings1::mixed_int_real_constraints_allowed = false
static

Definition at line 31 of file VSSettings.h.

◆ moduleName

constexpr auto smtrat::VSSettings1::moduleName = "VSModule<VSSettings1>"
staticconstexpr

Definition at line 18 of file VSSettings.h.

◆ only_split_in_final_call

const bool smtrat::VSSettings1::only_split_in_final_call = true
static

Definition at line 37 of file VSSettings.h.

◆ prefer_equation_over_all

const bool smtrat::VSSettings1::prefer_equation_over_all = false
static

Definition at line 30 of file VSSettings.h.

◆ split_neq_constraints

const bool smtrat::VSSettings1::split_neq_constraints = false
static

Definition at line 32 of file VSSettings.h.

◆ sturm_sequence_for_root_check

const bool smtrat::VSSettings1::sturm_sequence_for_root_check = use_variable_bounds && false
static

Definition at line 25 of file VSSettings.h.

◆ try_first_lazy

const bool smtrat::VSSettings1::try_first_lazy = false
static

Definition at line 35 of file VSSettings.h.

◆ use_backjumping

const bool smtrat::VSSettings1::use_backjumping = true
static

Definition at line 21 of file VSSettings.h.

◆ use_branch_and_bound

const bool smtrat::VSSettings1::use_branch_and_bound = true
static

Definition at line 36 of file VSSettings.h.

◆ use_fixed_variable_order

const bool smtrat::VSSettings1::use_fixed_variable_order = false
static

Definition at line 39 of file VSSettings.h.

◆ use_strict_inequalities_for_test_candidate_generation

const bool smtrat::VSSettings1::use_strict_inequalities_for_test_candidate_generation = true
static

Definition at line 22 of file VSSettings.h.

◆ use_variable_bounds

const bool smtrat::VSSettings1::use_variable_bounds = true
static

Definition at line 23 of file VSSettings.h.

◆ variable_valuation_strategy

constexpr auto smtrat::VSSettings1::variable_valuation_strategy = VariableValuationStrategy::OPTIMIZE_BEST
staticconstexpr

Definition at line 40 of file VSSettings.h.

◆ virtual_substitution_according_paper

const bool smtrat::VSSettings1::virtual_substitution_according_paper = false
static

Definition at line 29 of file VSSettings.h.

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