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

#include <SATSettings.h>

Inheritance diagram for smtrat::SATSettingsStopAfterUnknown:
Inheritance graph
[legend]
Collaboration diagram for smtrat::SATSettingsStopAfterUnknown:
Collaboration graph
[legend]

Public Types

using VarScheduler = VarSchedulerSMTTheoryGuided< TheoryGuidedDecisionHeuristicLevel::SATISFIED_FIRST >
 
using MCSATSettings = mcsat::MCSATSettingsFMVSNL
 

Static Public Attributes

static const bool stop_search_after_first_unknown = true
 
static constexpr auto moduleName = "SATModule<SATSettings1>"
 
static const bool allow_theory_propagation = true
 
static const bool try_full_lazy_call_first = false
 
static const bool use_restarts = true
 
static const bool formula_guided_decision_heuristic = false
 
static const bool check_active_literal_occurrences = false
 
static const bool check_if_all_clauses_are_satisfied = false
 
static const bool initiate_activities = false
 
static const bool remove_satisfied = false
 
static constexpr double percentage_of_conflicts_to_add = 1.0
 
static constexpr CCES conflict_clause_evaluation_strategy = CCES::SECOND_LEVEL_MINIMIZER_PLUS_LBD
 
static constexpr VARIABLE_ACTIVITY_STRATEGY initial_variable_activities = VARIABLE_ACTIVITY_STRATEGY::NONE
 
static const bool mc_sat = false
 
static constexpr bool validate_clauses = false
 
static constexpr bool check_for_duplicate_clauses = false
 
static constexpr bool mcsat_resolve_clause_chains = false
 
static constexpr bool mcsat_learn_lazy_explanations = false
 
static constexpr unsigned int mcsat_num_insert_assignments = 1
 
static constexpr MCSAT_BOOLEAN_DOMAIN_PROPAGATION mcsat_boolean_domain_propagation = MCSAT_BOOLEAN_DOMAIN_PROPAGATION::FULL
 
static constexpr bool mcsat_backjump_decide = true
 

Detailed Description

Definition at line 118 of file SATSettings.h.

Member Typedef Documentation

◆ MCSATSettings

using smtrat::SATSettings1::MCSATSettings = mcsat::MCSATSettingsFMVSNL
inherited

Definition at line 110 of file SATSettings.h.

◆ VarScheduler

using smtrat::SATSettings1::VarScheduler = VarSchedulerSMTTheoryGuided<TheoryGuidedDecisionHeuristicLevel::SATISFIED_FIRST>
inherited

Definition at line 108 of file SATSettings.h.

Field Documentation

◆ allow_theory_propagation

const bool smtrat::SATSettings1::allow_theory_propagation = true
staticinherited

Definition at line 29 of file SATSettings.h.

◆ check_active_literal_occurrences

const bool smtrat::SATSettings1::check_active_literal_occurrences = false
staticinherited

Definition at line 49 of file SATSettings.h.

◆ check_for_duplicate_clauses

constexpr bool smtrat::SATSettings1::check_for_duplicate_clauses = false
staticconstexprinherited

Definition at line 96 of file SATSettings.h.

◆ check_if_all_clauses_are_satisfied

const bool smtrat::SATSettings1::check_if_all_clauses_are_satisfied = false
staticinherited

Definition at line 53 of file SATSettings.h.

◆ conflict_clause_evaluation_strategy

constexpr CCES smtrat::SATSettings1::conflict_clause_evaluation_strategy = CCES::SECOND_LEVEL_MINIMIZER_PLUS_LBD
staticconstexprinherited

Definition at line 83 of file SATSettings.h.

◆ formula_guided_decision_heuristic

const bool smtrat::SATSettings1::formula_guided_decision_heuristic = false
staticinherited

Definition at line 45 of file SATSettings.h.

◆ initial_variable_activities

constexpr VARIABLE_ACTIVITY_STRATEGY smtrat::SATSettings1::initial_variable_activities = VARIABLE_ACTIVITY_STRATEGY::NONE
staticconstexprinherited

Definition at line 87 of file SATSettings.h.

◆ initiate_activities

const bool smtrat::SATSettings1::initiate_activities = false
staticinherited

Definition at line 57 of file SATSettings.h.

◆ mc_sat

const bool smtrat::SATSettings1::mc_sat = false
staticinherited

Definition at line 91 of file SATSettings.h.

◆ mcsat_backjump_decide

constexpr bool smtrat::SATSettings1::mcsat_backjump_decide = true
staticconstexprinherited

Definition at line 106 of file SATSettings.h.

◆ mcsat_boolean_domain_propagation

constexpr MCSAT_BOOLEAN_DOMAIN_PROPAGATION smtrat::SATSettings1::mcsat_boolean_domain_propagation = MCSAT_BOOLEAN_DOMAIN_PROPAGATION::FULL
staticconstexprinherited

Definition at line 104 of file SATSettings.h.

◆ mcsat_learn_lazy_explanations

constexpr bool smtrat::SATSettings1::mcsat_learn_lazy_explanations = false
staticconstexprinherited

Definition at line 100 of file SATSettings.h.

◆ mcsat_num_insert_assignments

constexpr unsigned int smtrat::SATSettings1::mcsat_num_insert_assignments = 1
staticconstexprinherited

Definition at line 102 of file SATSettings.h.

◆ mcsat_resolve_clause_chains

constexpr bool smtrat::SATSettings1::mcsat_resolve_clause_chains = false
staticconstexprinherited

Definition at line 98 of file SATSettings.h.

◆ moduleName

constexpr auto smtrat::SATSettings1::moduleName = "SATModule<SATSettings1>"
staticconstexprinherited

Definition at line 25 of file SATSettings.h.

◆ percentage_of_conflicts_to_add

constexpr double smtrat::SATSettings1::percentage_of_conflicts_to_add = 1.0
staticconstexprinherited

Definition at line 79 of file SATSettings.h.

◆ remove_satisfied

const bool smtrat::SATSettings1::remove_satisfied = false
staticinherited

Definition at line 61 of file SATSettings.h.

◆ stop_search_after_first_unknown

const bool smtrat::SATSettingsStopAfterUnknown::stop_search_after_first_unknown = true
static

Definition at line 120 of file SATSettings.h.

◆ try_full_lazy_call_first

const bool smtrat::SATSettings1::try_full_lazy_call_first = false
staticinherited

Definition at line 33 of file SATSettings.h.

◆ use_restarts

const bool smtrat::SATSettings1::use_restarts = true
staticinherited

Definition at line 37 of file SATSettings.h.

◆ validate_clauses

constexpr bool smtrat::SATSettings1::validate_clauses = false
staticconstexprinherited

Definition at line 93 of file SATSettings.h.

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