SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Data Fields
smtrat::mcsat::InformationGetter Struct Reference

#include <MCSATMixin.h>

Data Fields

std::function< Minisat::lbool(Minisat::Var)> getVarValue
 
std::function< Minisat::lbool(Minisat::Lit)> getLitValue
 
std::function< Minisat::lbool(Minisat::Var)> getBoolVarValue
 
std::function< int(Minisat::Var)> getDecisionLevel
 
std::function< int(Minisat::Var)> getTrailIndex
 
std::function< Minisat::CRef(Minisat::Var)> getReason
 
std::function< const Minisat::Clause &(Minisat::CRef)> getClause
 
std::function< const Minisat::vec< Minisat::CRef > &()> getClauses
 
std::function< const Minisat::vec< Minisat::CRef > &()> getLearntClauses
 
std::function< bool(Minisat::Var)> isTheoryAbstraction
 
std::function< bool(const FormulaT &)> isAbstractedFormula
 
std::function< Minisat::Var(const FormulaT &)> abstractVariable
 
std::function< const FormulaT &(Minisat::Var)> reabstractVariable
 
std::function< const FormulaT &(Minisat::Lit)> reabstractLiteral
 
std::function< const Minisat::vec< Minisat::Watcher > &(Minisat::Lit)> getWatches
 
std::function< Minisat::Var()> newVar
 

Detailed Description

Definition at line 24 of file MCSATMixin.h.

Field Documentation

◆ abstractVariable

std::function<Minisat::Var(const FormulaT&)> smtrat::mcsat::InformationGetter::abstractVariable

Definition at line 36 of file MCSATMixin.h.

◆ getBoolVarValue

std::function<Minisat::lbool(Minisat::Var)> smtrat::mcsat::InformationGetter::getBoolVarValue

Definition at line 27 of file MCSATMixin.h.

◆ getClause

std::function<const Minisat::Clause&(Minisat::CRef)> smtrat::mcsat::InformationGetter::getClause

Definition at line 31 of file MCSATMixin.h.

◆ getClauses

std::function<const Minisat::vec<Minisat::CRef>&()> smtrat::mcsat::InformationGetter::getClauses

Definition at line 32 of file MCSATMixin.h.

◆ getDecisionLevel

std::function<int(Minisat::Var)> smtrat::mcsat::InformationGetter::getDecisionLevel

Definition at line 28 of file MCSATMixin.h.

◆ getLearntClauses

std::function<const Minisat::vec<Minisat::CRef>&()> smtrat::mcsat::InformationGetter::getLearntClauses

Definition at line 33 of file MCSATMixin.h.

◆ getLitValue

std::function<Minisat::lbool(Minisat::Lit)> smtrat::mcsat::InformationGetter::getLitValue

Definition at line 26 of file MCSATMixin.h.

◆ getReason

std::function<Minisat::CRef(Minisat::Var)> smtrat::mcsat::InformationGetter::getReason

Definition at line 30 of file MCSATMixin.h.

◆ getTrailIndex

std::function<int(Minisat::Var)> smtrat::mcsat::InformationGetter::getTrailIndex

Definition at line 29 of file MCSATMixin.h.

◆ getVarValue

std::function<Minisat::lbool(Minisat::Var)> smtrat::mcsat::InformationGetter::getVarValue

Definition at line 25 of file MCSATMixin.h.

◆ getWatches

std::function<const Minisat::vec<Minisat::Watcher>&(Minisat::Lit)> smtrat::mcsat::InformationGetter::getWatches

Definition at line 39 of file MCSATMixin.h.

◆ isAbstractedFormula

std::function<bool(const FormulaT&)> smtrat::mcsat::InformationGetter::isAbstractedFormula

Definition at line 35 of file MCSATMixin.h.

◆ isTheoryAbstraction

std::function<bool(Minisat::Var)> smtrat::mcsat::InformationGetter::isTheoryAbstraction

Definition at line 34 of file MCSATMixin.h.

◆ newVar

std::function<Minisat::Var()> smtrat::mcsat::InformationGetter::newVar

Definition at line 40 of file MCSATMixin.h.

◆ reabstractLiteral

std::function<const FormulaT&(Minisat::Lit)> smtrat::mcsat::InformationGetter::reabstractLiteral

Definition at line 38 of file MCSATMixin.h.

◆ reabstractVariable

std::function<const FormulaT&(Minisat::Var)> smtrat::mcsat::InformationGetter::reabstractVariable

Definition at line 37 of file MCSATMixin.h.

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