SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
#include <Explanation.h>
Public Member Functions | |
std::optional< mcsat::Explanation > | operator() (const mcsat::Bookkeeping &trail, carl::Variable var, const FormulasT &trailLiterals, bool) const |
Definition at line 95 of file Explanation.h.
std::optional< mcsat::Explanation > smtrat::mcsat::onecellcad::recursive::Explanation< Setting1, Setting2 >::operator() | ( | const mcsat::Bookkeeping & | trail, |
carl::Variable | var, | ||
const FormulasT & | trailLiterals, | ||
bool | |||
) | const |