SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Private Attributes
smtrat::mcsat::MCSATBackend< Settings > Class Template Reference

#include <BaseBackend.h>

Inheritance diagram for smtrat::mcsat::MCSATBackend< Settings >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::mcsat::MCSATBackend< Settings >:
Collaboration graph
[legend]

Public Member Functions

void pushConstraint (const FormulaT &f)
 
void popConstraint (const FormulaT &f)
 
void pushAssignment (carl::Variable v, const ModelValue &mv, const FormulaT &f)
 
void popAssignment (carl::Variable v)
 
const auto & getModel () const
 
const auto & getTrail () const
 
void initVariables (const carl::Variables &variables)
 
const auto & variables () const
 
const auto & assignedVariables () const
 
AssignmentOrConflict findAssignment (carl::Variable var) const
 
AssignmentOrConflict isInfeasible (carl::Variable var, const FormulaT &f)
 
Explanation explain (carl::Variable var, const FormulasT &reason, bool force_use_core=false) const
 
Explanation explain (carl::Variable var, const FormulaT &f, const FormulasT &reason)
 
bool isActive (const FormulaT &f) const
 

Private Attributes

mcsat::Bookkeeping mBookkeeping
 
Settings::AssignmentFinderBackend mAssignmentFinder
 
Settings::ExplanationBackend mExplanation
 

Detailed Description

template<typename Settings>
class smtrat::mcsat::MCSATBackend< Settings >

Definition at line 14 of file BaseBackend.h.

Member Function Documentation

◆ assignedVariables()

template<typename Settings >
const auto& smtrat::mcsat::MCSATBackend< Settings >::assignedVariables ( ) const
inline

Definition at line 51 of file BaseBackend.h.

Here is the call graph for this function:

◆ explain() [1/2]

template<typename Settings >
Explanation smtrat::mcsat::MCSATBackend< Settings >::explain ( carl::Variable  var,
const FormulasT &  reason,
bool  force_use_core = false 
) const
inline

Definition at line 79 of file BaseBackend.h.

Here is the call graph for this function:

◆ explain() [2/2]

template<typename Settings >
Explanation smtrat::mcsat::MCSATBackend< Settings >::explain ( carl::Variable  var,
const FormulaT &  f,
const FormulasT &  reason 
)
inline

Definition at line 135 of file BaseBackend.h.

Here is the call graph for this function:

◆ findAssignment()

template<typename Settings >
AssignmentOrConflict smtrat::mcsat::MCSATBackend< Settings >::findAssignment ( carl::Variable  var) const
inline

Definition at line 55 of file BaseBackend.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getModel()

template<typename Settings >
const auto& smtrat::mcsat::MCSATBackend< Settings >::getModel ( ) const
inline

Definition at line 36 of file BaseBackend.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getTrail()

template<typename Settings >
const auto& smtrat::mcsat::MCSATBackend< Settings >::getTrail ( ) const
inline

Definition at line 39 of file BaseBackend.h.

Here is the caller graph for this function:

◆ initVariables()

template<typename Settings >
void smtrat::mcsat::MCSATBackend< Settings >::initVariables ( const carl::Variables &  variables)
inline

Definition at line 43 of file BaseBackend.h.

Here is the call graph for this function:

◆ isActive()

template<typename Settings >
bool smtrat::mcsat::MCSATBackend< Settings >::isActive ( const FormulaT &  f) const
inline

Definition at line 142 of file BaseBackend.h.

◆ isInfeasible()

template<typename Settings >
AssignmentOrConflict smtrat::mcsat::MCSATBackend< Settings >::isInfeasible ( carl::Variable  var,
const FormulaT &  f 
)
inline

Definition at line 66 of file BaseBackend.h.

Here is the call graph for this function:

◆ popAssignment()

template<typename Settings >
void smtrat::mcsat::MCSATBackend< Settings >::popAssignment ( carl::Variable  v)
inline

Definition at line 32 of file BaseBackend.h.

Here is the call graph for this function:

◆ popConstraint()

template<typename Settings >
void smtrat::mcsat::MCSATBackend< Settings >::popConstraint ( const FormulaT &  f)
inline

Definition at line 24 of file BaseBackend.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ pushAssignment()

template<typename Settings >
void smtrat::mcsat::MCSATBackend< Settings >::pushAssignment ( carl::Variable  v,
const ModelValue &  mv,
const FormulaT &  f 
)
inline

Definition at line 28 of file BaseBackend.h.

Here is the call graph for this function:

◆ pushConstraint()

template<typename Settings >
void smtrat::mcsat::MCSATBackend< Settings >::pushConstraint ( const FormulaT &  f)
inline

Definition at line 20 of file BaseBackend.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ variables()

template<typename Settings >
const auto& smtrat::mcsat::MCSATBackend< Settings >::variables ( ) const
inline

Definition at line 47 of file BaseBackend.h.

Here is the call graph for this function:
Here is the caller graph for this function:

Field Documentation

◆ mAssignmentFinder

template<typename Settings >
Settings::AssignmentFinderBackend smtrat::mcsat::MCSATBackend< Settings >::mAssignmentFinder
private

Definition at line 16 of file BaseBackend.h.

◆ mBookkeeping

template<typename Settings >
mcsat::Bookkeeping smtrat::mcsat::MCSATBackend< Settings >::mBookkeeping
private

Definition at line 15 of file BaseBackend.h.

◆ mExplanation

template<typename Settings >
Settings::ExplanationBackend smtrat::mcsat::MCSATBackend< Settings >::mExplanation
private

Definition at line 17 of file BaseBackend.h.

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