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

#include <BCAll.h>

Inheritance diagram for smtrat::internal::SATSettings::MCSATSettings:
Inheritance graph
[legend]
Collaboration diagram for smtrat::internal::SATSettings::MCSATSettings:
Collaboration graph
[legend]

Public Types

using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< OCSettings >, mcsat::nlsat::Explanation >
 
using AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder
 
using ExplanationBackend = mcsat::SequentialExplanation< mcsat::onecell::Explanation< smtrat::mcsat::onecell::DefaultSettings >, mcsat::nlsat::Explanation >
 

Static Public Attributes

static constexpr bool early_evaluation = false
 

Detailed Description

Definition at line 26 of file BCAll.h.

Member Typedef Documentation

◆ AssignmentFinderBackend [1/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 27 of file BCAll.h.

◆ AssignmentFinderBackend [2/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 27 of file BCBc.h.

◆ AssignmentFinderBackend [3/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCBoundsOnly.h.

◆ AssignmentFinderBackend [4/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCDeg10.h.

◆ AssignmentFinderBackend [5/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCDeg2.h.

◆ AssignmentFinderBackend [6/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCDeg5.h.

◆ AssignmentFinderBackend [7/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 27 of file BCIndep.h.

◆ AssignmentFinderBackend [8/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCIntersect.h.

◆ AssignmentFinderBackend [9/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCIrred.h.

◆ AssignmentFinderBackend [10/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCIrredIndep.h.

◆ AssignmentFinderBackend [11/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file BCNoop.h.

◆ AssignmentFinderBackend [12/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file BCRational.h.

◆ AssignmentFinderBackend [13/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 28 of file LDBBoundsOnly.h.

◆ AssignmentFinderBackend [14/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file LDBNoop.h.

◆ AssignmentFinderBackend [15/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 17 of file OCNew.cpp.

◆ AssignmentFinderBackend [16/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file OCNewBC.h.

◆ AssignmentFinderBackend [17/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file OCNewLDB.h.

◆ AssignmentFinderBackend [18/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file OCNewLDBCovering.h.

◆ AssignmentFinderBackend [19/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file OCNewLDBCoveringCache.h.

◆ AssignmentFinderBackend [20/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 23 of file OCNewLDBCoveringCacheGlobal.h.

◆ AssignmentFinderBackend [21/21]

using smtrat::internal::SATSettings::MCSATSettings::AssignmentFinderBackend = mcsat::arithmetic::AssignmentFinder

Definition at line 12 of file PPOCNew.h.

◆ ExplanationBackend [1/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 28 of file BCAll.h.

◆ ExplanationBackend [2/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 28 of file BCBc.h.

◆ ExplanationBackend [3/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCBoundsOnly.h.

◆ ExplanationBackend [4/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCDeg10.h.

◆ ExplanationBackend [5/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCDeg2.h.

◆ ExplanationBackend [6/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCDeg5.h.

◆ ExplanationBackend [7/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 28 of file BCIndep.h.

◆ ExplanationBackend [8/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCIntersect.h.

◆ ExplanationBackend [9/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCIrred.h.

◆ ExplanationBackend [10/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCIrredIndep.h.

◆ ExplanationBackend [11/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file BCNoop.h.

◆ ExplanationBackend [12/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file BCRational.h.

◆ ExplanationBackend [13/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 29 of file LDBBoundsOnly.h.

◆ ExplanationBackend [14/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file LDBNoop.h.

◆ ExplanationBackend [15/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 18 of file OCNew.cpp.

◆ ExplanationBackend [16/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file OCNewBC.h.

◆ ExplanationBackend [17/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file OCNewLDB.h.

◆ ExplanationBackend [18/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file OCNewLDBCovering.h.

◆ ExplanationBackend [19/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file OCNewLDBCoveringCache.h.

◆ ExplanationBackend [20/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<OCSettings>, mcsat::nlsat::Explanation>

Definition at line 24 of file OCNewLDBCoveringCacheGlobal.h.

◆ ExplanationBackend [21/21]

using smtrat::internal::SATSettings::MCSATSettings::ExplanationBackend = mcsat::SequentialExplanation<mcsat::onecell::Explanation<smtrat::mcsat::onecell::DefaultSettings>, mcsat::nlsat::Explanation>

Definition at line 13 of file PPOCNew.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 files: