Searched defs:satContext (Results 1 – 7 of 7) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | decision_strategy.cpp | 25 DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext, in DecisionStrategyFmf()
127 context::Context* satContext, in DecisionStrategySingleton()
|
| H A D | decision_manager.cpp | 25 DecisionManager::DecisionManager(context::Context* satContext) {} in DecisionManager()
|
| H A D | theory.cpp | 56 context::Context* satContext, in Theory()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | prop_engine.cpp | 78 PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, in PropEngine()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.cpp | 445 Node t, context::Context* satContext, Valuation valuation) in CardinalityDecisionStrategy()
1628 CombinedCardinalityDecisionStrategy(context::Context* satContext, in CombinedCardinalityDecisionStrategy()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.cpp | 998 context::Context* satContext, Valuation valuation) in SygusStreamDecisionStrategy()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/arith/ |
| H A D | constraint.cpp | 794 ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext,… in ConstraintDatabase()
1637 ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext): in Watches()
|