smtrat::mcsat::Bookkeeping Class Reference

Represent the trail, i.e. More...

#include <Bookkeeping.h>

Collaboration diagram for smtrat::mcsat::Bookkeeping:

Public Member Functions
const auto &	model () const
const auto &	assignedVariables () const
const auto &	assignments () const
const auto &	constraints () const
const auto &	mvBounds () const
const auto &	variables () const
void	updateVariables (const carl::Variables &variables)
void	pushConstraint (const FormulaT &f)
	Assert a constraint/literal. More...
void	popConstraint (const FormulaT &f)
void	pushAssignment (carl::Variable v, const ModelValue &mv, const FormulaT &f)
void	popAssignment (carl::Variable v)

Private Attributes
Model	mModel
	Current (partial) model. More...
std::vector< carl::Variable >	mAssignedVariables
	Stack of (algebraic) variables being assigned. More...
std::vector< FormulaT >	mAssignments
	Stack of theory assignments, i.e. More...
std::vector< FormulaT >	mConstraints
	Stack of asserted constraints/literals. More...
std::vector< FormulaT >	mMVBounds
	Stack of asserted multivariate root bounds. More...
carl::Variables	mVariables
	Set of theory variables. More...

Detailed Description

Represent the trail, i.e.

the assignment/model state, of a MCSAT run in different representations (kept in sync) for a fast access. Most notably, we store literals, i.e. a polynomial (in)equality-atom or its negation, which we assert to be true. Since the negation can be represented by an atom by flipping the (in)equality, it suffices to store only atoms. Here we call atomic formulas over the theory of real arithmetic "constraints".

Definition at line 19 of file Bookkeeping.h.

Member Function Documentation

assignedVariables()

const auto& smtrat::mcsat::Bookkeeping::assignedVariables ( ) const

inline

Definition at line 37 of file Bookkeeping.h.

Here is the caller graph for this function:

assignments()

const auto& smtrat::mcsat::Bookkeeping::assignments ( ) const

inline

Definition at line 40 of file Bookkeeping.h.

Here is the caller graph for this function:

constraints()

const auto& smtrat::mcsat::Bookkeeping::constraints ( ) const

inline

Definition at line 43 of file Bookkeeping.h.

Here is the caller graph for this function:

model()

const auto& smtrat::mcsat::Bookkeeping::model ( ) const

inline

Definition at line 34 of file Bookkeeping.h.

Here is the caller graph for this function:

mvBounds()

const auto& smtrat::mcsat::Bookkeeping::mvBounds ( ) const

inline

Definition at line 46 of file Bookkeeping.h.

Here is the caller graph for this function:

popAssignment()

void smtrat::mcsat::Bookkeeping::popAssignment ( carl::Variable  v )

inline

Definition at line 98 of file Bookkeeping.h.

Here is the caller graph for this function:

popConstraint()

void smtrat::mcsat::Bookkeeping::popConstraint ( const FormulaT &  f )

inline

Definition at line 73 of file Bookkeeping.h.

Here is the caller graph for this function:

pushAssignment()

void smtrat::mcsat::Bookkeeping::pushAssignment ( carl::Variable  v, const ModelValue &  mv, const FormulaT &  f  )

inline

Definition at line 90 of file Bookkeeping.h.

Here is the caller graph for this function:

pushConstraint()

void smtrat::mcsat::Bookkeeping::pushConstraint ( const FormulaT &  f )

inline

Assert a constraint/literal.

Definition at line 58 of file Bookkeeping.h.

Here is the caller graph for this function:

updateVariables()

void smtrat::mcsat::Bookkeeping::updateVariables ( const carl::Variables &  variables )

inline

Definition at line 53 of file Bookkeeping.h.

Here is the call graph for this function:

Here is the caller graph for this function:

variables()

const auto& smtrat::mcsat::Bookkeeping::variables ( ) const

inline

Definition at line 49 of file Bookkeeping.h.

Here is the caller graph for this function:

Field Documentation

mAssignedVariables

std::vector<carl::Variable> smtrat::mcsat::Bookkeeping::mAssignedVariables

private

Stack of (algebraic) variables being assigned.

Definition at line 23 of file Bookkeeping.h.

mAssignments

std::vector<FormulaT> smtrat::mcsat::Bookkeeping::mAssignments

private

Stack of theory assignments, i.e.

the values for the variables.

Definition at line 25 of file Bookkeeping.h.

mConstraints

std::vector<FormulaT> smtrat::mcsat::Bookkeeping::mConstraints

private

Stack of asserted constraints/literals.

Definition at line 27 of file Bookkeeping.h.

mModel

Model smtrat::mcsat::Bookkeeping::mModel

private

Current (partial) model.

Definition at line 21 of file Bookkeeping.h.

mMVBounds

std::vector<FormulaT> smtrat::mcsat::Bookkeeping::mMVBounds

private

Stack of asserted multivariate root bounds.

Definition at line 29 of file Bookkeeping.h.

mVariables

carl::Variables smtrat::mcsat::Bookkeeping::mVariables

private

Set of theory variables.

Definition at line 31 of file Bookkeeping.h.

---

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

• smtrat-mcsat/utils/Bookkeeping.h