SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
AssignmentFinder.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "../../smtrat-mcsat.h"
4 
5 #include "AAFStatistics.h"
6 
7 namespace smtrat {
8 namespace mcsat {
9 namespace arithmetic {
10 
11 struct AssignmentFinder {
12 
13 #ifdef SMTRAT_DEVOPTION_Statistics
14  AAFStatistics& mStatistics = statistics_get<AAFStatistics>("mcsat-assignment-arithmetic");
15 #endif
16 
17  std::optional<AssignmentOrConflict> operator()(const mcsat::Bookkeeping& data, carl::Variable var) const;
18  bool active(const mcsat::Bookkeeping& data, const FormulaT& f) const;
19 };
20 
21 }
22 }
23 }
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::FormulaT
carl::Formula< Poly > FormulaT
Definition: types.h:37
smtrat::mcsat::arithmetic::AssignmentFinder::active
bool active(const mcsat::Bookkeeping &data, const FormulaT &f) const
Definition: AssignmentFinder.cpp:52
smtrat::mcsat::arithmetic::AssignmentFinder::operator()
std::optional< AssignmentOrConflict > operator()(const mcsat::Bookkeeping &data, carl::Variable var) const
Definition: AssignmentFinder.cpp:10