| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | decision_strategy.cpp | 25 DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext, in DecisionStrategyFmf() argument
28 d_has_curr_literal(false, satContext), in DecisionStrategyFmf()
29 d_curr_literal(0, satContext) in DecisionStrategyFmf()
127 context::Context* satContext, in DecisionStrategySingleton() argument
129 : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit) in DecisionStrategySingleton()
|
| H A D | theory.cpp | 56 context::Context* satContext, in Theory() argument
64 d_satContext(satContext), in Theory()
67 d_facts(satContext), in Theory()
68 d_factsHead(satContext, 0), in Theory()
69 d_sharedTermsIndex(satContext, 0), in Theory()
77 d_sharedTerms(satContext), in Theory()
|
| H A D | decision_strategy.h | 71 DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
124 context::Context* satContext,
|
| H A D | decision_manager.h | 86 DecisionManager(context::Context* satContext);
|
| H A D | decision_manager.cpp | 25 DecisionManager::DecisionManager(context::Context* satContext) {} in DecisionManager() argument
|
| H A D | theory.h | 198 context::Context* satContext,
|
| /dports/math/cvc4/CVC4-1.7/src/prop/ |
| H A D | prop_engine.h | 101 PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext,
|
| H A D | prop_engine.cpp | 78 PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, in PropEngine() argument
84 d_context(satContext), in PropEngine()
|
| /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() argument
796 , d_toPropagate(satContext) in ConstraintDatabase()
797 , d_antecedents(satContext, false) in ConstraintDatabase()
798 , d_watches(new Watches(satContext, userContext)) in ConstraintDatabase()
801 , d_satContext(satContext) in ConstraintDatabase()
1637 ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Context* userContext): in Watches() argument
1638 d_constraintProofs(satContext), in Watches()
1639 d_canBePropagatedWatches(satContext), in Watches()
1640 d_assertionOrderWatches(satContext), in Watches()
|
| H A D | congruence_manager.h | 148 …ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, co…
|
| H A D | constraint.h | 1050 Watches(context::Context* satContext, context::Context* userContext);
1085 ConstraintDatabase( context::Context* satContext,
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf_strong_solver.h | 347 context::Context* satContext,
452 CombinedCardinalityDecisionStrategy(context::Context* satContext,
|
| H A D | theory_uf_strong_solver.cpp | 445 Node t, context::Context* satContext, Valuation valuation) in CardinalityDecisionStrategy() argument
446 : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t) in CardinalityDecisionStrategy()
1628 CombinedCardinalityDecisionStrategy(context::Context* satContext, in CombinedCardinalityDecisionStrategy() argument
1630 : DecisionStrategyFmf(satContext, valuation) in CombinedCardinalityDecisionStrategy()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.h | 346 SygusStreamDecisionStrategy(context::Context* satContext,
|
| H A D | synth_conjecture.cpp | 998 context::Context* satContext, Valuation valuation) in SygusStreamDecisionStrategy() argument
999 : DecisionStrategyFmf(satContext, valuation) in SygusStreamDecisionStrategy()
|