Base class for solvers.
More...
#include <Manager.h>
Inherited by smtrat::AllModulesStrategy, smtrat::BVPreprocessing, smtrat::BVSolver, smtrat::CSplitFull, smtrat::CSplitModule< Settings >::LAModule, smtrat::CSplitOnly, smtrat::CoveringNG_Default, smtrat::CoveringNG_GBDefault, smtrat::CoveringNG_PPBooleanExploration, smtrat::CoveringNG_PPBooleanExplorationOnlyBool, smtrat::CoveringNG_PPBooleanExplorationWithBool, smtrat::CoveringNG_PPBooleanOff, smtrat::CoveringNG_PPBooleanPartialPropagationSotd, smtrat::CoveringNG_PPBooleanPartialPropagationTdeg, smtrat::CoveringNG_PPBooleanPropagation, smtrat::CoveringNG_PPDefault, smtrat::CoveringNG_PPFilterBoundsOnly, smtrat::CoveringNG_PPFilterBoundsOnlyComplete, smtrat::CoveringNG_PPFilterNoop, smtrat::CoveringNG_PPGBDefault, smtrat::CoveringNG_PPImplicantsLevelSize, smtrat::CoveringNG_PPImplicantsLevelSotd, smtrat::CoveringNG_PPImplicantsPickeringTotal, smtrat::CoveringNG_PPImplicantsSizeOnly, smtrat::CoveringNG_PPImplicantsSotd, smtrat::CoveringNG_PPImplicantsSotdReverse, smtrat::CoveringNG_PPImplicantsTdeg, smtrat::CoveringNG_PPImplicantsVars, smtrat::CoveringNG_PPImplicantsVarsVarorderSplitting, smtrat::CoveringNG_PPInprocessingOn, smtrat::CoveringNG_PPSTropDefault, smtrat::CoveringNG_PPVarorderPickering, smtrat::CoveringNG_PPVarorderUnivariate, smtrat::Default, smtrat::DefaultTwo, smtrat::Filter_BCAll, smtrat::Filter_BCBc, smtrat::Filter_BCBoundsOnly, smtrat::Filter_BCDeg10, smtrat::Filter_BCDeg2, smtrat::Filter_BCDeg5, smtrat::Filter_BCIndep, smtrat::Filter_BCIntersect, smtrat::Filter_BCIrred, smtrat::Filter_BCIrredIndep, smtrat::Filter_BCNoop, smtrat::Filter_BCRational, smtrat::Filter_LDBBoundsOnly, smtrat::Filter_LDBNoop, smtrat::LIASolver, smtrat::LRASolver, smtrat::MAXSATBackendStrategy, smtrat::MCSAT_FMICPOC, smtrat::MCSAT_FMICPVSNL, smtrat::MCSAT_FMICPVSOC, smtrat::MCSAT_FMICPVSOCLWH11, smtrat::MCSAT_FMICPVSOCLWH12, smtrat::MCSAT_FMICPVSOCLWH13, smtrat::MCSAT_FMICPVSOCNNASC, smtrat::MCSAT_FMICPVSOCNNDSC, smtrat::MCSAT_FMICPVSOCNew, smtrat::MCSAT_FMICPVSOCNewOC, smtrat::MCSAT_FMICPVSOCPARALLEL, smtrat::MCSAT_FMNL, smtrat::MCSAT_FMOCNew, smtrat::MCSAT_FMVSNL, smtrat::MCSAT_FMVSOC, smtrat::MCSAT_ICPNL, smtrat::MCSAT_NL, smtrat::MCSAT_OC, smtrat::MCSAT_OCLWH11, smtrat::MCSAT_OCLWH12, smtrat::MCSAT_OCLWH13, smtrat::MCSAT_OCLWH21, smtrat::MCSAT_OCLWH22, smtrat::MCSAT_OCLWH23, smtrat::MCSAT_OCLWH31, smtrat::MCSAT_OCLWH32, smtrat::MCSAT_OCLWH33, smtrat::MCSAT_OCNN, smtrat::MCSAT_OCNNASC, smtrat::MCSAT_OCNNDSC, smtrat::MCSAT_OCNew, smtrat::MCSAT_OCNewBC, smtrat::MCSAT_OCNewLDB, smtrat::MCSAT_OCNewLDBCovering, smtrat::MCSAT_OCNewLDBCoveringCache, smtrat::MCSAT_OCNewLDBCoveringCacheGlobal, smtrat::MCSAT_OCPARALLEL, smtrat::MCSAT_PPDefault, smtrat::MCSAT_PPNL, smtrat::MCSAT_PPOC, smtrat::MCSAT_PPOCNew, smtrat::MCSAT_VSNL, smtrat::MCSAT_VSOCNew, smtrat::MIS_Exact, smtrat::MIS_Greedy, smtrat::MIS_GreedyPre, smtrat::MIS_GreedyWeighted, smtrat::MIS_Hybrid, smtrat::MIS_Trivial, smtrat::MIS_Trivial, smtrat::NIABB, smtrat::NIABlast, smtrat::NIASolver, smtrat::NRARefinement_Solver, smtrat::NRARefinement_Solver1, smtrat::NRARefinement_Solver10, smtrat::NRARefinement_Solver11, smtrat::NRARefinement_Solver12, smtrat::NRARefinement_Solver13, smtrat::NRARefinement_Solver14, smtrat::NRARefinement_Solver15, smtrat::NRARefinement_Solver16, smtrat::NRARefinement_Solver17, smtrat::NRARefinement_Solver18, smtrat::NRARefinement_Solver19, smtrat::NRARefinement_Solver2, smtrat::NRARefinement_Solver20, smtrat::NRARefinement_Solver21, smtrat::NRARefinement_Solver22, smtrat::NRARefinement_Solver23, smtrat::NRARefinement_Solver24, smtrat::NRARefinement_Solver25, smtrat::NRARefinement_Solver3, smtrat::NRARefinement_Solver4, smtrat::NRARefinement_Solver5, smtrat::NRARefinement_Solver6, smtrat::NRARefinement_Solver7, smtrat::NRARefinement_Solver8, smtrat::NRARefinement_Solver9, smtrat::NRASolver, smtrat::NRASolverCov, smtrat::NRA_CAD, smtrat::NRA_ICPVSCAD, smtrat::NRA_LRAVSCAD, smtrat::NRA_VSCAD, smtrat::NewCADEQ_B, smtrat::NewCADEQ_BD, smtrat::NewCADEQ_BR, smtrat::NewCADEQ_BRD, smtrat::NewCADEQ_BRI, smtrat::NewCADEQ_BRID, smtrat::NewCADEQ_BS, smtrat::NewCADEQ_BSD, smtrat::NewCADEQ_BSI, smtrat::NewCADEQ_BSID, smtrat::NewCADEQ_R, smtrat::NewCADEQ_RD, smtrat::NewCADEQ_RI, smtrat::NewCADEQ_RID, smtrat::NewCADEQ_S, smtrat::NewCADEQ_SD, smtrat::NewCADEQ_SI, smtrat::NewCADEQ_SID, smtrat::NewCAD_Brown, smtrat::NewCAD_Collins, smtrat::NewCAD_FOS, smtrat::NewCAD_FU, smtrat::NewCAD_FU_SC, smtrat::NewCAD_FU_SI, smtrat::NewCAD_FU_SInf, smtrat::NewCAD_FU_SL, smtrat::NewCAD_FU_SR, smtrat::NewCAD_FU_SZ, smtrat::NewCAD_Hong, smtrat::NewCAD_LOLS, smtrat::NewCAD_LOLT, smtrat::NewCAD_LOLTA, smtrat::NewCAD_LOLTS, smtrat::NewCAD_LOLTSA, smtrat::NewCAD_LOS, smtrat::NewCAD_LOT, smtrat::NewCAD_LOTLSA, smtrat::NewCAD_LOTS, smtrat::NewCAD_LOTSA, smtrat::NewCAD_McCallum, smtrat::NewCAD_McCallumPartial, smtrat::NewCAD_NO, smtrat::NewCAD_NU, smtrat::NewCAD_Naive, smtrat::NewCAD_Only, smtrat::NewCAD_POD, smtrat::NewCAD_POLD, smtrat::NewCAD_POPD, smtrat::NewCAD_POSD, smtrat::NewCAD_PP, smtrat::NewCAD_PPRR, smtrat::NewCAD_PPVE, smtrat::NewCAD_PPVERR, smtrat::NewCAD_SAT, smtrat::NewCAD_SO, smtrat::NewCAD_SU, smtrat::NewCovering_Backtracking, smtrat::NewCovering_FilterBoundsOnly, smtrat::NewCovering_Incomplete, smtrat::NewCovering_Incremental, smtrat::NewCovering_IncrementalBacktracking, smtrat::NewCovering_PPComplete, smtrat::NewCovering_PPFilterBoundsOnly, smtrat::NewCovering_PPFilterBoundsOnlyComplete, smtrat::NewCovering_PPIncomplete, smtrat::NewCovering_Vanilla, smtrat::OnlyCAD, smtrat::OnlyGB, smtrat::OnlySAT, smtrat::OnlySATPP, smtrat::OnlyVS, smtrat::OptimizationPreprocessing, smtrat::OptimizationStrategy, smtrat::PBPPStrategy, smtrat::PBPPStrategy, smtrat::PBPPStrategy2, smtrat::PBPPStrategyBasic, smtrat::PBPPStrategyGauss, smtrat::PBPPStrategyGroe_Norm_PB_LIA, smtrat::PBPPStrategyGroe_PB_LIA, smtrat::PBPPStrategyGroebner, smtrat::PBPPStrategyLIA, smtrat::PBPPStrategyLIAOnly, smtrat::PBPPStrategyLIA_ICP, smtrat::PBPPStrategyLIA_VS, smtrat::PBPPStrategyNorm_LIA, smtrat::PBPPStrategyNorm_LIA_ICP, smtrat::PBPPStrategyNorm_LIA_VS, smtrat::PBPPStrategyNorm_PB_LIA, smtrat::PBPPStrategyPB_LIA, smtrat::PBPPStrategyRNS, smtrat::PBPPStrategyWithCardConstr, smtrat::PBPPStrategyWithMixedConstr, smtrat::PBPreprocessing, smtrat::PBPreprocessingGroebner, smtrat::PreprocessingOne, smtrat::PreprocessingTwo, smtrat::RatIntBlast, smtrat::SMTCOMP, smtrat::STropModule< Settings >::LAModule, smtrat::STrop_BackendsOnly, smtrat::STrop_CADBackendsOnly, smtrat::STrop_Formula, smtrat::STrop_FormulaAlt, smtrat::STrop_FormulaAltOutputOnly, smtrat::STrop_FormulaAltWCADBackends, smtrat::STrop_FormulaAltWCADBackendsFull, smtrat::STrop_FormulaOutputOnly, smtrat::STrop_FormulaWBackends, smtrat::STrop_FormulaWBackendsFull, smtrat::STrop_FormulaWCADBackends, smtrat::STrop_FormulaWCADBackendsFull, smtrat::STrop_FormulaWMCSAT, smtrat::STrop_Incremental, smtrat::STrop_IncrementalWBackends, smtrat::STrop_IncrementalWCADBackends, smtrat::STrop_MCSATOnly, smtrat::STrop_TransformationEQ, smtrat::STrop_TransformationEQOutputOnly, smtrat::STrop_TransformationEQWBackends, smtrat::STrop_TransformationEQWCADBackends, and smtrat::mcsat::smtaf::SMTModule.
Base class for solvers.
This is the interface to the user.
Definition at line 33 of file Manager.h.
◆ Manager()
| smtrat::Manager::Manager |
( |
| ) |
|
◆ ~Manager()
| smtrat::Manager::~Manager |
( |
| ) |
|
◆ add()
| bool smtrat::Manager::add |
( |
const FormulaT & |
_subformula, |
|
|
bool |
_containsUnknownConstraints = true |
|
) |
| |
Adds the given formula to the conjunction of formulas, which will be considered for the next satisfiability check.
- Parameters
-
| _subformula | The formula to add. |
| _containsUnknownConstraints | true, if the formula to add contains constraints, about which this solver was not yet informed. |
- Returns
- false, if it is easy to decide whether adding this formula creates a conflict; true, otherwise.
Definition at line 86 of file Manager.cpp.
◆ addBackend() [1/2]
template<typename Module >
◆ addBackend() [2/2]
template<typename Module >
◆ addEdge()
| BackendLink& smtrat::Manager::addEdge |
( |
std::size_t |
from, |
|
|
std::size_t |
to |
|
) |
| |
|
inlineprotected |
◆ addInformationRelevantFormula()
| void smtrat::Manager::addInformationRelevantFormula |
( |
const FormulaT & |
formula | ) |
|
|
inline |
Adds formula to InformationRelevantFormula.
- Parameters
-
Definition at line 319 of file Manager.h.
◆ allModels()
| const std::vector<Model>& smtrat::Manager::allModels |
( |
| ) |
const |
|
inline |
- Returns
- A list of all assignments, such that they satisfy the conjunction of the so far added formulas.
Note, that an assignment is only provided if the conjunction of so far added formulas is satisfiable. Furthermore, when solving non-linear real arithmetic formulas the assignment could contain other variables or freshly introduced variables.
Definition at line 213 of file Manager.h.
◆ check()
| Answer smtrat::Manager::check |
( |
bool |
_full = true | ) |
|
Checks the so far added formulas for satisfiability.
- Returns
- True, if the conjunction of the so far added formulas is satisfiable; False, if it not satisfiable; Unknown, if this solver cannot decide whether it is satisfiable or not.
Definition at line 115 of file Manager.cpp.
◆ clear()
| void smtrat::Manager::clear |
( |
| ) |
|
|
inline |
◆ clearInformationRelevantFormula()
| void smtrat::Manager::clearInformationRelevantFormula |
( |
| ) |
|
|
inline |
Deletes all InformationRelevantFormula.
Definition at line 327 of file Manager.h.
◆ deinform()
| void smtrat::Manager::deinform |
( |
const FormulaT & |
_constraint | ) |
|
The inverse of informing about a constraint.
All data structures which were kept regarding this constraint are going to be removed. Note, that this makes only sense if it is not likely enough that a formula with this constraint must be solved again.
- Parameters
-
| _constraint | The constraint to remove from internal data structures. |
Definition at line 81 of file Manager.cpp.
◆ formula()
- Returns
- The conjunction of so far added formulas.
Definition at line 229 of file Manager.h.
◆ formulaBegin()
◆ formulaEnd()
◆ getAllBackends()
| std::vector<Module*> smtrat::Manager::getAllBackends |
( |
Module * |
_module | ) |
const |
|
inlineprotected |
Gets all backends so far instantiated according the strategy and all previous enquiries of the given module.
- Parameters
-
| _module | The module to get all backends so far instantiated according the strategy and all previous enquiries of this module. |
- Returns
- All backends so far instantiated according the strategy and all previous enquiries of the given module.
Definition at line 411 of file Manager.h.
◆ getAllGeneratedModules()
| const std::vector<Module*>& smtrat::Manager::getAllGeneratedModules |
( |
| ) |
const |
|
inline |
- Returns
- All instantiated modules of the solver belonging to this manager.
Definition at line 288 of file Manager.h.
◆ getBackends()
| std::vector< Module * > smtrat::Manager::getBackends |
( |
Module * |
_requiredBy, |
|
|
std::atomic_bool * |
_foundAnswer |
|
) |
| |
|
protected |
Get the backends to call for the given problem instance required by the given module.
- Parameters
-
| _requiredBy | The module asking for a backend. |
| _foundAnswer | A conditional |
- Returns
- A vector of modules, which the module defined by _requiredBy calls in parallel to achieve an answer to the given instance.
Definition at line 279 of file Manager.cpp.
◆ getInformationRelevantFormulas()
| const std::set<FormulaT>& smtrat::Manager::getInformationRelevantFormulas |
( |
| ) |
|
|
inlineprotected |
Gets all InformationRelevantFormulas.
- Returns
- Set of all formulas
Definition at line 460 of file Manager.h.
◆ getInputSimplified()
| std::pair< bool, FormulaT > smtrat::Manager::getInputSimplified |
( |
| ) |
|
- Returns
- A pair of a Boolean and a formula, where the Boolean is true, if the input formula could be simplified to an equisatisfiable formula. The formula is equisatisfiable to this solver's input formula, if the Boolean is true.
Definition at line 149 of file Manager.cpp.
◆ getModelEqualities()
| std::list< std::vector< carl::Variable > > smtrat::Manager::getModelEqualities |
( |
| ) |
const |
Determines variables assigned by the currently found satisfying assignment to an equal value in their domain.
- Returns
- A list of vectors of variables, stating that the variables in one vector are assigned to equal values.
Definition at line 127 of file Manager.cpp.
◆ infeasibleSubsets()
| const std::vector< FormulaSetT > & smtrat::Manager::infeasibleSubsets |
( |
| ) |
const |
- Returns
- All infeasible subsets of the set so far added formulas.
Note, that the conjunction of the so far added formulas must be inconsistent to receive an infeasible subset.
Definition at line 122 of file Manager.cpp.
◆ inform()
| bool smtrat::Manager::inform |
( |
const FormulaT & |
_constraint | ) |
|
Informs the solver about a constraint.
Optimally, it should be informed about all constraints, which it will receive eventually, before any of them is added as part of a formula with the interface add(..).
- Parameters
-
| _constraint | The constraint to inform about. |
- Returns
- false, if it is easy to decide (for any module used of this solver), whether the constraint itself is inconsistent; true, otherwise.
Definition at line 76 of file Manager.cpp.
◆ isLemmaLevel()
| bool smtrat::Manager::isLemmaLevel |
( |
LemmaLevel |
level | ) |
|
|
inline |
Checks if current lemma level is greater or equal to given level.
- Parameters
-
Definition at line 345 of file Manager.h.
◆ lemmas()
| std::vector< FormulaT > smtrat::Manager::lemmas |
( |
| ) |
|
Returns the lemmas/tautologies which were made during the last solving provoked by check().
These lemmas can be used in the same manner as infeasible subsets are used.
- Returns
- The lemmas/tautologies made during solving.
Definition at line 138 of file Manager.cpp.
◆ logic()
| auto smtrat::Manager::logic |
( |
| ) |
const |
|
inline |
- Returns
- A constant reference to the logic this solver considers.
Definition at line 304 of file Manager.h.
◆ model()
| const Model & smtrat::Manager::model |
( |
| ) |
const |
- Returns
- An assignment of the variables, which occur in the so far added formulas, to values of their domains, such that it satisfies the conjunction of these formulas.
Note, that an assignment is only provided if the conjunction of so far added formulas is satisfiable. Furthermore, when solving non-linear real arithmetic formulas the assignment could contain other variables or freshly introduced variables.
Definition at line 132 of file Manager.cpp.
◆ objectiveVariable()
| const carl::Variable& smtrat::Manager::objectiveVariable |
( |
| ) |
const |
|
inline |
◆ pop() [1/2]
| bool smtrat::Manager::pop |
( |
void |
| ) |
|
Pops a backtrack point from the stack of backtrack points.
This provokes, that all formulas which have been added after that backtrack point are removed.
Note, that this interface has not necessarily be used to apply a solver constructed with SMT-RAT, but is often required by state-of-the-art SMT solvers when embedding a theory solver constructed with SMT-RAT into them.
Definition at line 166 of file Manager.cpp.
◆ pop() [2/2]
| void smtrat::Manager::pop |
( |
size_t |
_levels | ) |
|
◆ printAllAssignments()
| void smtrat::Manager::printAllAssignments |
( |
std::ostream & |
_out = std::cout | ) |
|
|
inline |
Prints all assignments of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable.
- Parameters
-
| _out | The stream to print on. |
Definition at line 257 of file Manager.h.
◆ printAssignment()
| void smtrat::Manager::printAssignment |
( |
| ) |
const |
Prints the currently found assignment of variables occurring in the so far added formulas to values of their domains, if the conjunction of these formulas is satisfiable.
Definition at line 154 of file Manager.cpp.
◆ printBackTrackStack()
| void smtrat::Manager::printBackTrackStack |
( |
std::ostream & |
_out = std::cout | ) |
const |
Prints the stack of backtrack points.
- Parameters
-
| _out | The stream to print on. |
Definition at line 258 of file Manager.cpp.
◆ printInfeasibleSubset()
| void smtrat::Manager::printInfeasibleSubset |
( |
std::ostream & |
_out = std::cout | ) |
const |
Prints the first found infeasible subset of the set of received formulas.
- Parameters
-
| _out | The stream to print on. |
Definition at line 237 of file Manager.cpp.
◆ printStrategyGraph()
| void smtrat::Manager::printStrategyGraph |
( |
std::ostream & |
_out = std::cout | ) |
const |
|
inline |
Prints the strategy of the solver maintained by this manager.
- Parameters
-
| _out | The stream to print on. |
Definition at line 278 of file Manager.h.
◆ push()
| void smtrat::Manager::push |
( |
void |
| ) |
|
|
inline |
Pushes a backtrack point to the stack of backtrack points.
Note, that this interface has not necessarily be used to apply a solver constructed with SMT-RAT, but is often required by state-of-the-art SMT solvers when embedding a theory solver constructed with SMT-RAT into them.
Definition at line 142 of file Manager.h.
◆ rDebugOutputChannel()
| std::ostream& smtrat::Manager::rDebugOutputChannel |
( |
| ) |
|
|
inline |
- Returns
- The stream to print the debug information on.
Definition at line 296 of file Manager.h.
◆ remove() [1/2]
Temporarily added: (TODO: Discuss with Gereon) Removes the given formula in the conjunction of formulas, which will be considered for the next satisfiability check.
- Parameters
-
| _subformula | The formula to remove. |
- Returns
- An iterator to the formula after the position of the just removed formula. If the removed formula has been the last element, the end of the conjunction of formulas, which will be considered for the next satisfiability check is returned.
Definition at line 378 of file Manager.h.
◆ remove() [2/2]
Removes the formula at the given position in the conjunction of formulas, which will be considered for the next satisfiability check.
- Parameters
-
| _subformula | The position of the formula to remove. |
- Returns
- An iterator to the formula after the position of the just removed formula. If the removed formula has been the last element, the end of the conjunction of formulas, which will be considered for the next satisfiability check is returned.
Definition at line 159 of file Manager.cpp.
◆ reset()
| void smtrat::Manager::reset |
( |
| ) |
|
◆ rLogic()
| auto& smtrat::Manager::rLogic |
( |
| ) |
|
|
inline |
- Returns
- A reference to the logic this solver considers.
Definition at line 311 of file Manager.h.
◆ setLemmaLevel()
| void smtrat::Manager::setLemmaLevel |
( |
LemmaLevel |
level | ) |
|
|
inline |
Sets the current level for lemma generation.
- Parameters
-
Definition at line 336 of file Manager.h.
◆ setObjectiveVariable()
| void smtrat::Manager::setObjectiveVariable |
( |
carl::Variable |
var | ) |
|
|
inline |
◆ setStrategy() [1/2]
| void smtrat::Manager::setStrategy |
( |
const BackendLink & |
backend | ) |
|
|
inlineprotected |
◆ setStrategy() [2/2]
| void smtrat::Manager::setStrategy |
( |
const std::initializer_list< BackendLink > & |
backends | ) |
|
|
inlineprotected |
◆ Module
◆ mBackendsOfModules
| std::map<const Module* const, std::vector<Module*> > smtrat::Manager::mBackendsOfModules |
|
private |
a mapping of each module to its backends
Definition at line 49 of file Manager.h.
◆ mBackendsUptodate
| bool smtrat::Manager::mBackendsUptodate |
|
private |
a Boolean showing whether the manager has received new constraint after the last consistency check
Definition at line 53 of file Manager.h.
◆ mBacktrackPoints
Contains the backtrack points, that are iterators to the last formula to be kept when backtracking to the respective point.
Definition at line 45 of file Manager.h.
◆ mDebugOutputChannel
| std::ostream smtrat::Manager::mDebugOutputChannel |
|
private |
channel to write debug output
Definition at line 57 of file Manager.h.
◆ mGeneratedModules
| std::vector<Module*> smtrat::Manager::mGeneratedModules |
|
private |
all generated instances of modules
Definition at line 47 of file Manager.h.
◆ mInformationRelevantFormula
| std::set<FormulaT> smtrat::Manager::mInformationRelevantFormula |
|
private |
List of formula which are relevant for certain tasks.
Definition at line 61 of file Manager.h.
◆ mLemmaLevel
Level of lemma generation.
Definition at line 63 of file Manager.h.
◆ mLogic
| carl::Logic smtrat::Manager::mLogic |
|
private |
the logic this solver considers
Definition at line 59 of file Manager.h.
◆ mObjectiveVariable
| carl::Variable smtrat::Manager::mObjectiveVariable |
|
private |
objective variable
Definition at line 65 of file Manager.h.
◆ mpPassedFormula
the constraints so far passed to the primary backend
Definition at line 41 of file Manager.h.
◆ mpPrimaryBackend
| Module* smtrat::Manager::mpPrimaryBackend |
|
private |
the primary backends
Definition at line 51 of file Manager.h.
◆ mPrimaryBackendFoundAnswer
a vector of flags, which indicate that an answer has been found of an antecessor module of the primary module
Definition at line 39 of file Manager.h.
◆ mPropositions
| carl::Condition smtrat::Manager::mPropositions |
|
private |
The propositions of the passed formula.
Definition at line 43 of file Manager.h.
◆ mStrategyGraph
primary strategy
Definition at line 55 of file Manager.h.
The documentation for this class was generated from the following files:
1.9.1 
