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 &data, carl::Variable var, const FormulasT &reason, bool) const |
Definition at line 11 of file Explanation.h.
std::optional< mcsat::Explanation > smtrat::mcsat::vs::Explanation::operator() | ( | const mcsat::Bookkeeping & | data, |
carl::Variable | var, | ||
const FormulasT & | reason, | ||
bool | |||
) | const |