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

Public Member Functions

 lemma_lt (SATModule &solver)
 
int levelOf (Minisat::Var v)
 
bool operator() (Minisat::Lit x, Minisat::Lit y)
 

Data Fields

SATModule & solver
 

Detailed Description

template<class Settings>
struct smtrat::SATModule< Settings >::lemma_lt

Definition at line 248 of file SATModule.h.

Constructor & Destructor Documentation

◆ lemma_lt()

template<class Settings >
smtrat::SATModule< Settings >::lemma_lt::lemma_lt ( SATModule &  solver)
inline

Definition at line 251 of file SATModule.h.

Member Function Documentation

◆ levelOf()

template<class Settings >
int smtrat::SATModule< Settings >::lemma_lt::levelOf ( Minisat::Var  v)
inline

Definition at line 252 of file SATModule.h.

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

◆ operator()()

template<class Settings >
bool smtrat::SATModule< Settings >::lemma_lt::operator() ( Minisat::Lit  x,
Minisat::Lit  y 
)
inline

Definition at line 263 of file SATModule.h.

Here is the call graph for this function:

Field Documentation

◆ solver

template<class Settings >
SATModule& smtrat::SATModule< Settings >::lemma_lt::solver

Definition at line 250 of file SATModule.h.

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