SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields
smtrat::mcsat::MCSATMixin< Settings >::VarMapping Struct Reference
Collaboration diagram for smtrat::mcsat::MCSATMixin< Settings >::VarMapping:
Collaboration graph
[legend]

Public Member Functions

void insert (const carl::Variable &carlVar, Minisat::Var minisatVar)
 
bool has (Minisat::Var v) const
 
bool has (const carl::Variable &v) const
 
const carl::Variable & carlVar (Minisat::Var v) const
 
Minisat::Var minisatVar (const carl::Variable &v) const
 
std::vector< Minisat::Var > minisatVars () const
 

Data Fields

std::map< Minisat::Var, carl::Variable > minisatToCarl
 
std::map< carl::Variable, Minisat::Var > carlToMinisat
 

Detailed Description

template<typename Settings>
struct smtrat::mcsat::MCSATMixin< Settings >::VarMapping

Definition at line 81 of file MCSATMixin.h.

Member Function Documentation

◆ carlVar()

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

Definition at line 98 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ has() [1/2]

template<typename Settings >
bool smtrat::mcsat::MCSATMixin< Settings >::VarMapping::has ( const carl::Variable &  v) const
inline

Definition at line 94 of file MCSATMixin.h.

◆ has() [2/2]

template<typename Settings >
bool smtrat::mcsat::MCSATMixin< Settings >::VarMapping::has ( Minisat::Var  v) const
inline

Definition at line 90 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ insert()

template<typename Settings >
void smtrat::mcsat::MCSATMixin< Settings >::VarMapping::insert ( const carl::Variable &  carlVar,
Minisat::Var  minisatVar 
)
inline

Definition at line 85 of file MCSATMixin.h.

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

◆ minisatVar()

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

Definition at line 102 of file MCSATMixin.h.

Here is the caller graph for this function:

◆ minisatVars()

template<typename Settings >
std::vector<Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::VarMapping::minisatVars ( ) const
inline

Definition at line 106 of file MCSATMixin.h.

Here is the caller graph for this function:

Field Documentation

◆ carlToMinisat

template<typename Settings >
std::map<carl::Variable, Minisat::Var> smtrat::mcsat::MCSATMixin< Settings >::VarMapping::carlToMinisat

Definition at line 83 of file MCSATMixin.h.

◆ minisatToCarl

template<typename Settings >
std::map<Minisat::Var, carl::Variable> smtrat::mcsat::MCSATMixin< Settings >::VarMapping::minisatToCarl

Definition at line 82 of file MCSATMixin.h.

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