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

#include <MCSATSettings.h>

Inheritance diagram for smtrat::mcsat::MCSATSettingsFMICPVSOCNewOC:
Inheritance graph
[legend]
Collaboration diagram for smtrat::mcsat::MCSATSettingsFMICPVSOCNewOC:
Collaboration graph
[legend]

Public Types

using AssignmentFinderBackend = arithmetic::AssignmentFinder
 
using ExplanationBackend = SequentialExplanation< fm::Explanation< fm::DefaultSettings >, icp::Explanation, vs::Explanation, onecell::Explanation< onecell::DefaultSettings >, onecellcad::recursive::Explanation< onecellcad::recursive::CoverNullification, onecellcad::recursive::NoHeuristic >, nlsat::Explanation >
 

Static Public Attributes

static constexpr bool early_evaluation = false
 

Detailed Description

Definition at line 181 of file MCSATSettings.h.

Member Typedef Documentation

◆ AssignmentFinderBackend

using smtrat::mcsat::MCSATSettingsFMICPVSOCNewOC::AssignmentFinderBackend = arithmetic::AssignmentFinder

Definition at line 182 of file MCSATSettings.h.

◆ ExplanationBackend

using smtrat::mcsat::MCSATSettingsFMICPVSOCNewOC::ExplanationBackend = SequentialExplanation<fm::Explanation<fm::DefaultSettings>,icp::Explanation,vs::Explanation,onecell::Explanation<onecell::DefaultSettings>,onecellcad::recursive::Explanation<onecellcad::recursive::CoverNullification, onecellcad::recursive::NoHeuristic>,nlsat::Explanation>

Definition at line 183 of file MCSATSettings.h.

Field Documentation

◆ early_evaluation

constexpr bool smtrat::mcsat::Base::early_evaluation = false
staticconstexprinherited

Definition at line 21 of file MCSATSettings.h.

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