SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions
smtrat::sat::detail::ClauseChecker Struct Reference

#include <ClauseChecker.h>

Public Member Functions

Model buildModel () const
 
void operator() (const FormulaT &formula) const
 
void operator() (const FormulasT &formulas) const
 
template<typename VM , typename BCM >
void operator() (const Minisat::Clause &c, const VM &vm, const BCM &bcm) const
 

Detailed Description

Definition at line 10 of file ClauseChecker.h.

Member Function Documentation

◆ buildModel()

Model smtrat::sat::detail::ClauseChecker::buildModel ( ) const
inline

Definition at line 11 of file ClauseChecker.h.

Here is the caller graph for this function:

◆ operator()() [1/3]

void smtrat::sat::detail::ClauseChecker::operator() ( const FormulasT &  formulas) const
inline

Definition at line 27 of file ClauseChecker.h.

Here is the call graph for this function:

◆ operator()() [2/3]

void smtrat::sat::detail::ClauseChecker::operator() ( const FormulaT &  formula) const
inline

Definition at line 20 of file ClauseChecker.h.

◆ operator()() [3/3]

template<typename VM , typename BCM >
void smtrat::sat::detail::ClauseChecker::operator() ( const Minisat::Clause &  c,
const VM &  vm,
const BCM &  bcm 
) const
inline

Definition at line 42 of file ClauseChecker.h.

Here is the call graph for this function:
The documentation for this struct was generated from the following file: