smtrat::mcsat::smtaf::AssignmentFinder_SMT Class Reference

#include <AssignmentFinder_SMT.h>

Collaboration diagram for smtrat::mcsat::smtaf::AssignmentFinder_SMT:

Public Member Functions
	AssignmentFinder_SMT (VariableRange variables, const Model &model)
boost::tribool	addConstraint (const FormulaT &f)
boost::tribool	addMVBound (const FormulaT &f)
std::optional< AssignmentOrConflict >	findAssignment (const VariablePos excludeVar) const
std::optional< AssignmentOrConflict >	findAssignment () const

Private Member Functions
ModelValues	modelToAssignment (const Model &model) const
std::variant< VariablePos, bool >	level (const FormulaT &constraint) const

Private Attributes
VariableRange	mVariables
Model	mModel
std::map< VariablePos, FormulasT >	mConstraints
std::map< VariablePos, carl::Variables >	mFreeConstraintVars
std::unordered_map< FormulaT, FormulaT >	mEvaluatedConstraints

Detailed Description

Definition at line 16 of file AssignmentFinder_SMT.h.

Constructor & Destructor Documentation

AssignmentFinder_SMT()

smtrat::mcsat::smtaf::AssignmentFinder_SMT::AssignmentFinder_SMT ( VariableRange  variables, const Model &  model  )

inline

Definition at line 35 of file AssignmentFinder_SMT.h.

Member Function Documentation

addConstraint()

boost::tribool smtrat::mcsat::smtaf::AssignmentFinder_SMT::addConstraint

(

const FormulaT &

f

)

Definition at line 59 of file AssignmentFinder_SMT.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

addMVBound()

boost::tribool smtrat::mcsat::smtaf::AssignmentFinder_SMT::addMVBound

(

const FormulaT &

f

)

Definition at line 92 of file AssignmentFinder_SMT.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

findAssignment() [1/2]

std::optional< AssignmentOrConflict > smtrat::mcsat::smtaf::AssignmentFinder_SMT::findAssignment

(

)

const

Definition at line 231 of file AssignmentFinder_SMT.cpp.

findAssignment() [2/2]

std::optional< AssignmentOrConflict > smtrat::mcsat::smtaf::AssignmentFinder_SMT::findAssignment

(

const VariablePos

excludeVar

)

const

Definition at line 163 of file AssignmentFinder_SMT.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

level()

std::variant< VariablePos, bool > smtrat::mcsat::smtaf::AssignmentFinder_SMT::level ( const FormulaT &  constraint ) const

private

Returns

A VariablePos, if the level is in the current range. true, if the level is higher, false, if the level is lower

Definition at line 39 of file AssignmentFinder_SMT.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

modelToAssignment()

ModelValues smtrat::mcsat::smtaf::AssignmentFinder_SMT::modelToAssignment ( const Model &  model ) const

private

Definition at line 29 of file AssignmentFinder_SMT.cpp.

Here is the caller graph for this function:

Field Documentation

mConstraints

std::map<VariablePos,FormulasT> smtrat::mcsat::smtaf::AssignmentFinder_SMT::mConstraints

private

Definition at line 20 of file AssignmentFinder_SMT.h.

mEvaluatedConstraints

std::unordered_map<FormulaT,FormulaT> smtrat::mcsat::smtaf::AssignmentFinder_SMT::mEvaluatedConstraints

private

Definition at line 22 of file AssignmentFinder_SMT.h.

mFreeConstraintVars

std::map<VariablePos,carl::Variables> smtrat::mcsat::smtaf::AssignmentFinder_SMT::mFreeConstraintVars

private

Definition at line 21 of file AssignmentFinder_SMT.h.

mModel

Model smtrat::mcsat::smtaf::AssignmentFinder_SMT::mModel

private

Definition at line 19 of file AssignmentFinder_SMT.h.

mVariables

VariableRange smtrat::mcsat::smtaf::AssignmentFinder_SMT::mVariables

private

Definition at line 18 of file AssignmentFinder_SMT.h.

---

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

• smtrat-mcsat/assignments/smtaf/AssignmentFinder_SMT.h
• smtrat-mcsat/assignments/smtaf/AssignmentFinder_SMT.cpp