SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Static Public Attributes
smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings Struct Reference
Inheritance diagram for smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings:
Inheritance graph
[legend]
Collaboration diagram for smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings:
Collaboration graph
[legend]

Static Public Attributes

static constexpr cad::Incrementality incrementality = cad::Incrementality::NONE
 
static constexpr cad::Backtracking backtracking = cad::Backtracking::ORDERED
 
static constexpr cad::ProjectionType projectionOperator = cad::ProjectionType::Hong
 
static constexpr CoreHeuristic coreHeuristic = cad::CoreHeuristic::PreferProjection
 
static constexpr MISHeuristic misHeuristic = cad::MISHeuristic::GREEDY
 
static constexpr std::size_t trivialSampleRadius = 1
 
static constexpr bool simplifyProjectionByBounds = true
 
static constexpr ProjectionCompareStrategy projectionComparator = cad::ProjectionCompareStrategy::Default
 
static constexpr SampleCompareStrategy sampleComparator = cad::SampleCompareStrategy::Default
 
static constexpr FullSampleCompareStrategy fullSampleComparator = cad::FullSampleCompareStrategy::Default
 

Detailed Description

Definition at line 94 of file ExplanationGenerator.h.

Field Documentation

◆ backtracking

constexpr cad::Backtracking smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings::backtracking = cad::Backtracking::ORDERED
staticconstexpr

Definition at line 96 of file ExplanationGenerator.h.

◆ coreHeuristic

constexpr CoreHeuristic smtrat::cad::BaseSettings::coreHeuristic = cad::CoreHeuristic::PreferProjection
staticconstexprinherited

Definition at line 37 of file Settings.h.

◆ fullSampleComparator

constexpr FullSampleCompareStrategy smtrat::cad::BaseSettings::fullSampleComparator = cad::FullSampleCompareStrategy::Default
staticconstexprinherited

Definition at line 45 of file Settings.h.

◆ incrementality

constexpr cad::Incrementality smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings::incrementality = cad::Incrementality::NONE
staticconstexpr

Definition at line 95 of file ExplanationGenerator.h.

◆ misHeuristic

constexpr MISHeuristic smtrat::cad::BaseSettings::misHeuristic = cad::MISHeuristic::GREEDY
staticconstexprinherited

Definition at line 39 of file Settings.h.

◆ projectionComparator

constexpr ProjectionCompareStrategy smtrat::cad::BaseSettings::projectionComparator = cad::ProjectionCompareStrategy::Default
staticconstexprinherited

Definition at line 43 of file Settings.h.

◆ projectionOperator

constexpr cad::ProjectionType smtrat::mcsat::nlsat::ExplanationGenerator::ProjectionSettings::projectionOperator = cad::ProjectionType::Hong
staticconstexpr

Definition at line 97 of file ExplanationGenerator.h.

◆ sampleComparator

constexpr SampleCompareStrategy smtrat::cad::BaseSettings::sampleComparator = cad::SampleCompareStrategy::Default
staticconstexprinherited

Definition at line 44 of file Settings.h.

◆ simplifyProjectionByBounds

constexpr bool smtrat::cad::BaseSettings::simplifyProjectionByBounds = true
staticconstexprinherited

Definition at line 41 of file Settings.h.

◆ trivialSampleRadius

constexpr std::size_t smtrat::cad::BaseSettings::trivialSampleRadius = 1
staticconstexprinherited

Definition at line 40 of file Settings.h.

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