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