SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Explanation.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "VSStatistics.h"
4 
5 #include <smtrat-mcsat/smtrat-mcsat.h>
6 
7 namespace smtrat {
8 namespace mcsat {
9 namespace vs {
10 
11 struct Explanation {
12 
13 #ifdef SMTRAT_DEVOPTION_Statistics
14  VSStatistics& mStatistics = statistics_get<VSStatistics>("mcsat-explanation-vs");
15 #endif
16 
17  std::optional<mcsat::Explanation> operator()(const mcsat::Bookkeeping& data, carl::Variable var, const FormulasT& reason, bool) const;
18 };
19 
20 }
21 }
22 }
smtrat::mcsat::Bookkeeping
Represent the trail, i.e.
Definition: Bookkeeping.h:19
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:64
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::FormulasT
carl::Formulas< Poly > FormulasT
Definition: types.h:39
smtrat::mcsat::vs::Explanation::operator()
std::optional< mcsat::Explanation > operator()(const mcsat::Bookkeeping &data, carl::Variable var, const FormulasT &reason, bool) const
Definition: Explanation.cpp:9