#include <MCSATMixin.h>

Inheritance diagram for smtrat::mcsat::MCSATMixin< Settings >:

Collaboration diagram for smtrat::mcsat::MCSATMixin< Settings >:

[legend]

Data Structures
struct	VarMapping

struct	VarProperties

Public Member Functions
template<typename BaseModule >
	MCSATMixin (BaseModule &baseModule)

std::size_t	level () const

const Model &	model () const

const std::vector< Minisat::Var > &	undecidedBooleanVariables () const

bool	isAssignedTheoryVariable (const carl::Variable &var) const

bool	theoryAssignmentComplete () const

const TheoryLevel &	get (std::size_t level) const
	Returns the respective theory level. More...

const TheoryLevel &	current () const
	Returns the current theory level. More...

TheoryLevel &	current ()

carl::Variable	variable (std::size_t level) const
	Retrieve already decided theory variables. More...

void	doBooleanAssignment (Minisat::Lit lit)
	Add a new constraint. More...

void	undoBooleanAssignment (Minisat::Lit lit)
	Remove the last constraint. More...

std::size_t	addBooleanVariable (Minisat::Var variable)
	Add a variable, return the level it was inserted on. More...

Minisat::Var	topSemanticPropagation ()
	Getter for semantic propagations. More...

bool	isFormulaUnivariate (const FormulaT &formula, std::size_t level) const
	Checks whether the given formula is univariate on the given level. More...

void	pushTheoryDecision (const FormulaT &assignment, Minisat::Lit decisionLiteral)
	Push a theory decision. More...

bool	backtrackTo (Minisat::Lit literal)
	Backtracks to the theory decision represented by the given literal. More...

Minisat::lbool	evaluateLiteral (Minisat::Lit lit) const
	Evaluate a literal in the theory, set lastReason to last theory decision involved. More...

std::pair< bool, std::optional< Explanation > >	isBooleanDecisionFeasible (Minisat::Lit lit, bool always_explain=false)

std::pair< boost::tribool, std::optional< Explanation > >	propagateBooleanDomain (Minisat::Lit lit)

std::optional< Explanation >	isFeasible (const carl::Variable &var)

std::variant< Explanation, FormulasT >	makeTheoryDecision (const carl::Variable &var)

bool	is_consistent ()
	Checks if any inconsistency was detected. More...

bool	is_consistent (Minisat::Var v)

std::optional< Explanation >	explainInconsistency ()
	Checks if the trail is consistent after the assignment on the current level. More...

Explanation	explainTheoryPropagation (Minisat::Lit literal)

template<typename Constraints >
void	initVariables (const Constraints &c)

bool	isTheoryVar (Minisat::Var v) const

const carl::Variable &	carlVar (Minisat::Var v) const

Minisat::Var	minisatVar (const carl::Variable &v) const

std::vector< Minisat::Var >	theoryVarAbstractions () const

bool	hasUnassignedDep (Minisat::Var v) const

std::size_t	theoryLevel (Minisat::Var var) const

std::size_t	computeTheoryLevel (Minisat::Var var) const

std::size_t	computeTheoryLevel (const FormulaT &f) const

Minisat::Lit	getDecisionLiteral (Minisat::Var var) const

int	assignedAtTrailIndex (Minisat::Var variable) const

int	decisionLevel (Minisat::Var v) const

bool	fullConsistencyCheck () const

std::size_t	maxDegree (const Minisat::Var &var)

std::vector< Minisat::Var >	theoryVars (const Minisat::Var &var)

void	printClause (std::ostream &os, Minisat::CRef clause) const
	Prints a single clause. More...

Private Types
using	TheoryStackT = std::vector< TheoryLevel >
	The first entry of the stack always contains an entry for the non-theory variables: the variable is set to NO_VARIABLE and the lists contain variables that do not contain any theory variables. More...

Private Member Functions
void	updateCurrentLevel ()
	Updates lookup for the current level. More...

void	popTheoryDecision ()
	Pop a theory decision. More...

std::size_t	varid (Minisat::Var var) const

Private Attributes
InformationGetter	mGetter

TheoryStackT	mTheoryStack

std::vector< size_t >	mTheoryLevels
	Theory levels for Boolean variables. More...

std::vector< Minisat::Var >	mUndecidedVariables
	Variables that are not univariate in any variable yet. More...

std::vector< Minisat::Var >	mInconsistentVariables
	Variables that are inconsistent in the current theory level. More...

std::set< Minisat::Var >	mSemanticPropagations
	Semantically propagated variables that are not yet inserted into the trail. More...

std::map< Minisat::Var, std::vector< Minisat::Var > >	mVarDeps

MCSATBackend< Settings >	mBackend

VarMapping	mTheoryVarMapping

std::vector< VarProperties >	mVarPropertyCache
	Cache for static information about variables. More...

Friends
template<typename Sett >
std::ostream &	operator<< (std::ostream &os, const MCSATMixin< Sett > &mcm)

Detailed Description

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

Definition at line 52 of file MCSATMixin.h.

Member Typedef Documentation

◆ TheoryStackT

template<typename Settings >

using smtrat::mcsat::MCSATMixin< Settings >::TheoryStackT = std::vector<TheoryLevel>

private

The first entry of the stack always contains an entry for the non-theory variables: the variable is set to NO_VARIABLE and the lists contain variables that do not contain any theory variables.

Definition at line 62 of file MCSATMixin.h.

Constructor & Destructor Documentation

◆ MCSATMixin()

template<typename Settings >

template<typename BaseModule >

smtrat::mcsat::MCSATMixin< Settings >::MCSATMixin ( BaseModule & baseModule )

inlineexplicit

Definition at line 182 of file MCSATMixin.h.

Here is the call graph for this function:

Member Function Documentation

◆ addBooleanVariable()

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::addBooleanVariable ( Minisat::Var variable )

Add a variable, return the level it was inserted on.

◆ assignedAtTrailIndex()

template<typename Settings >

int smtrat::mcsat::MCSATMixin< Settings >::assignedAtTrailIndex ( Minisat::Var variable ) const

inline

Definition at line 581 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ backtrackTo()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::backtrackTo ( Minisat::Lit literal )

Backtracks to the theory decision represented by the given literal.

◆ carlVar()

template<typename Settings >

const carl::Variable& smtrat::mcsat::MCSATMixin< Settings >::carlVar ( Minisat::Var v ) const

inline

Definition at line 494 of file MCSATMixin.h.

Here is the call graph for this function:

◆ computeTheoryLevel() [1/2]

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::computeTheoryLevel ( const FormulaT & f ) const

inline

Definition at line 532 of file MCSATMixin.h.

Here is the call graph for this function:

◆ computeTheoryLevel() [2/2]

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::computeTheoryLevel ( Minisat::Var var ) const

inline

Definition at line 525 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ current() [1/2]

template<typename Settings >

TheoryLevel& smtrat::mcsat::MCSATMixin< Settings >::current ( )

inline

Definition at line 232 of file MCSATMixin.h.

◆ current() [2/2]

template<typename Settings >

const TheoryLevel& smtrat::mcsat::MCSATMixin< Settings >::current ( ) const

inline

Returns the current theory level.

Definition at line 229 of file MCSATMixin.h.

◆ decisionLevel()

template<typename Settings >

int smtrat::mcsat::MCSATMixin< Settings >::decisionLevel ( Minisat::Var v ) const

inline

Definition at line 590 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ doBooleanAssignment()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::doBooleanAssignment ( Minisat::Lit lit )

inline

Add a new constraint.

Definition at line 248 of file MCSATMixin.h.

Here is the call graph for this function:

◆ evaluateLiteral()

template<typename Settings >

Minisat::lbool smtrat::mcsat::MCSATMixin< Settings >::evaluateLiteral ( Minisat::Lit lit ) const

Evaluate a literal in the theory, set lastReason to last theory decision involved.

Here is the caller graph for this function:

◆ explainInconsistency()

template<typename Settings >

std::optional<Explanation> smtrat::mcsat::MCSATMixin< Settings >::explainInconsistency ( )

inline

Checks if the trail is consistent after the assignment on the current level.

The trail must be consistent on the previous level.

Returns std::nullopt if consistent and an explanation.

Definition at line 396 of file MCSATMixin.h.

Here is the call graph for this function:

◆ explainTheoryPropagation()

template<typename Settings >

Explanation smtrat::mcsat::MCSATMixin< Settings >::explainTheoryPropagation ( Minisat::Lit literal )

inline

Definition at line 419 of file MCSATMixin.h.

Here is the call graph for this function:

◆ fullConsistencyCheck()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::fullConsistencyCheck ( ) const

inline

Definition at line 601 of file MCSATMixin.h.

Here is the call graph for this function:

◆ get()

template<typename Settings >

const TheoryLevel& smtrat::mcsat::MCSATMixin< Settings >::get ( std::size_t level ) const

inline

Returns the respective theory level.

Definition at line 224 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getDecisionLiteral()

template<typename Settings >

Minisat::Lit smtrat::mcsat::MCSATMixin< Settings >::getDecisionLiteral ( Minisat::Var var ) const

inline

Definition at line 571 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ hasUnassignedDep()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::hasUnassignedDep ( Minisat::Var v ) const

inline

Definition at line 506 of file MCSATMixin.h.

◆ initVariables()

template<typename Settings >

template<typename Constraints >

void smtrat::mcsat::MCSATMixin< Settings >::initVariables ( const Constraints & c )

inline

Definition at line 453 of file MCSATMixin.h.

Here is the call graph for this function:

◆ is_consistent() [1/2]

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::is_consistent ( )

inline

Checks if any inconsistency was detected.

Definition at line 382 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ is_consistent() [2/2]

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::is_consistent ( Minisat::Var v )

inline

Definition at line 386 of file MCSATMixin.h.

Here is the call graph for this function:

◆ isAssignedTheoryVariable()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::isAssignedTheoryVariable ( const carl::Variable & var ) const

inline

Definition at line 217 of file MCSATMixin.h.

Here is the call graph for this function:

◆ isBooleanDecisionFeasible()

template<typename Settings >

std::pair<bool, std::optional<Explanation> > smtrat::mcsat::MCSATMixin< Settings >::isBooleanDecisionFeasible	(	Minisat::Lit	lit,
		bool	always_explain = `false`
	)

◆ isFeasible()

template<typename Settings >

std::optional<Explanation> smtrat::mcsat::MCSATMixin< Settings >::isFeasible ( const carl::Variable & var )

inline

Definition at line 325 of file MCSATMixin.h.

Here is the call graph for this function:

◆ isFormulaUnivariate()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::isFormulaUnivariate	(	const FormulaT &	formula,
		std::size_t	level
	)		const

Checks whether the given formula is univariate on the given level.

◆ isTheoryVar()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::isTheoryVar ( Minisat::Var v ) const

inline

Definition at line 490 of file MCSATMixin.h.

Here is the call graph for this function:

◆ level()

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::level ( ) const

inline

Definition at line 208 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ makeTheoryDecision()

template<typename Settings >

std::variant<Explanation,FormulasT> smtrat::mcsat::MCSATMixin< Settings >::makeTheoryDecision ( const carl::Variable & var )

inline

Definition at line 348 of file MCSATMixin.h.

Here is the call graph for this function:

◆ maxDegree()

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::maxDegree ( const Minisat::Var & var )

inline

Definition at line 629 of file MCSATMixin.h.

Here is the call graph for this function:

◆ minisatVar()

template<typename Settings >

Minisat::Var smtrat::mcsat::MCSATMixin< Settings >::minisatVar ( const carl::Variable & v ) const

inline

Definition at line 498 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ model()

template<typename Settings >

const Model& smtrat::mcsat::MCSATMixin< Settings >::model ( ) const

inline

Definition at line 211 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ popTheoryDecision()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::popTheoryDecision ( )

private

Pop a theory decision.

◆ printClause()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::printClause	(	std::ostream &	os,
		Minisat::CRef	clause
	)		const

Prints a single clause.

◆ propagateBooleanDomain()

template<typename Settings >

std::pair<boost::tribool, std::optional<Explanation> > smtrat::mcsat::MCSATMixin< Settings >::propagateBooleanDomain ( Minisat::Lit lit )

◆ pushTheoryDecision()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::pushTheoryDecision	(	const FormulaT &	assignment,
		Minisat::Lit	decisionLiteral
	)

Push a theory decision.

◆ theoryAssignmentComplete()

template<typename Settings >

bool smtrat::mcsat::MCSATMixin< Settings >::theoryAssignmentComplete ( ) const

inline

Definition at line 220 of file MCSATMixin.h.

◆ theoryLevel()

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::theoryLevel ( Minisat::Var var ) const

inline

Definition at line 517 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ theoryVarAbstractions()

template<typename Settings >

std::vector<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::theoryVarAbstractions ( ) const

inline

Definition at line 502 of file MCSATMixin.h.

Here is the call graph for this function:

◆ theoryVars()

template<typename Settings >

std::vector<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::theoryVars ( const Minisat::Var & var )

inline

Definition at line 660 of file MCSATMixin.h.

Here is the call graph for this function:

◆ topSemanticPropagation()

template<typename Settings >

Minisat::Var smtrat::mcsat::MCSATMixin< Settings >::topSemanticPropagation ( )

inline

Getter for semantic propagations.

Definition at line 298 of file MCSATMixin.h.

◆ undecidedBooleanVariables()

template<typename Settings >

const std::vector<Minisat::Var>& smtrat::mcsat::MCSATMixin< Settings >::undecidedBooleanVariables ( ) const

inline

Definition at line 214 of file MCSATMixin.h.

◆ undoBooleanAssignment()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::undoBooleanAssignment ( Minisat::Lit lit )

inline

Remove the last constraint.

f must be the same as the one passed to the last call of pushConstraint().

Definition at line 275 of file MCSATMixin.h.

Here is the call graph for this function:

◆ updateCurrentLevel()

template<typename Settings >

void smtrat::mcsat::MCSATMixin< Settings >::updateCurrentLevel ( )

private

Updates lookup for the current level.

◆ variable()

template<typename Settings >

carl::Variable smtrat::mcsat::MCSATMixin< Settings >::variable ( std::size_t level ) const

inline

Retrieve already decided theory variables.

Definition at line 236 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ varid()

template<typename Settings >

std::size_t smtrat::mcsat::MCSATMixin< Settings >::varid ( Minisat::Var var ) const

inlineprivate

Definition at line 175 of file MCSATMixin.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

template<typename Settings >

template<typename Sett >

std::ostream& operator<<	(	std::ostream &	os,
		const MCSATMixin< Sett > &	mcm
	)

friend

Field Documentation

◆ mBackend

template<typename Settings >

MCSATBackend<Settings> smtrat::mcsat::MCSATMixin< Settings >::mBackend

private

Definition at line 79 of file MCSATMixin.h.

◆ mGetter

template<typename Settings >

InformationGetter smtrat::mcsat::MCSATMixin< Settings >::mGetter

private

Definition at line 55 of file MCSATMixin.h.

◆ mInconsistentVariables

template<typename Settings >

std::vector<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::mInconsistentVariables

private

Variables that are inconsistent in the current theory level.

Definition at line 72 of file MCSATMixin.h.

◆ mSemanticPropagations

template<typename Settings >

std::set<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::mSemanticPropagations

private

Semantically propagated variables that are not yet inserted into the trail.

Definition at line 75 of file MCSATMixin.h.

◆ mTheoryLevels

template<typename Settings >

std::vector<size_t> smtrat::mcsat::MCSATMixin< Settings >::mTheoryLevels

private

Theory levels for Boolean variables.

Definition at line 66 of file MCSATMixin.h.

◆ mTheoryStack

template<typename Settings >

TheoryStackT smtrat::mcsat::MCSATMixin< Settings >::mTheoryStack

private

Definition at line 63 of file MCSATMixin.h.

◆ mTheoryVarMapping

template<typename Settings >

VarMapping smtrat::mcsat::MCSATMixin< Settings >::mTheoryVarMapping

private

Definition at line 114 of file MCSATMixin.h.

◆ mUndecidedVariables

template<typename Settings >

std::vector<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::mUndecidedVariables

private

Variables that are not univariate in any variable yet.

Definition at line 69 of file MCSATMixin.h.

◆ mVarDeps

template<typename Settings >

std::map<Minisat::Var, std::vector<Minisat::Var> > smtrat::mcsat::MCSATMixin< Settings >::mVarDeps

private

Definition at line 77 of file MCSATMixin.h.

◆ mVarPropertyCache

template<typename Settings >

std::vector<VarProperties> smtrat::mcsat::MCSATMixin< Settings >::mVarPropertyCache

private

Cache for static information about variables.

Definition at line 165 of file MCSATMixin.h.

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

smtrat-modules/SATModule/mcsat/MCSATMixin.h

Data Structures

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends

Detailed Description

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

Member Typedef Documentation

◆ TheoryStackT

Constructor & Destructor Documentation

◆ MCSATMixin()

Member Function Documentation

◆ addBooleanVariable()

◆ assignedAtTrailIndex()

◆ backtrackTo()

◆ carlVar()

◆ computeTheoryLevel() [1/2]

◆ computeTheoryLevel() [2/2]

◆ current() [1/2]

◆ current() [2/2]

◆ decisionLevel()

◆ doBooleanAssignment()

◆ evaluateLiteral()

◆ explainInconsistency()

◆ explainTheoryPropagation()

◆ fullConsistencyCheck()

◆ get()

◆ getDecisionLiteral()

◆ hasUnassignedDep()

◆ initVariables()

◆ is_consistent() [1/2]

◆ is_consistent() [2/2]

◆ isAssignedTheoryVariable()

◆ isBooleanDecisionFeasible()

◆ isFeasible()

◆ isFormulaUnivariate()

◆ isTheoryVar()

◆ level()

◆ makeTheoryDecision()

◆ maxDegree()

◆ minisatVar()

◆ model()

◆ popTheoryDecision()

◆ printClause()

◆ propagateBooleanDomain()

◆ pushTheoryDecision()

◆ theoryAssignmentComplete()

◆ theoryLevel()

◆ theoryVarAbstractions()

◆ theoryVars()

◆ topSemanticPropagation()

◆ undecidedBooleanVariables()

◆ undoBooleanAssignment()

◆ updateCurrentLevel()

◆ variable()

◆ varid()

Friends And Related Function Documentation

◆ operator<<

Field Documentation

◆ mBackend

◆ mGetter

◆ mInconsistentVariables

◆ mSemanticPropagations

◆ mTheoryLevels

◆ mTheoryStack

◆ mTheoryVarMapping

◆ mUndecidedVariables

◆ mVarDeps

◆ mVarPropertyCache

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