| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | inst_strategy_enumerative.cpp | 59 void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) in check() argument
66 doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); in check()
70 doCheck = quant_e == QEFFORT_LAST_CALL; in check()
|
| H A D | inst_propagator.h | 122 bool notifyInstantiation(QuantifiersModule::QEffort quant_e, in notifyInstantiation() argument
128 return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); in notifyInstantiation()
134 bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
|
| H A D | inst_strategy_enumerative.h | 74 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | quant_split.cpp | 86 void QuantDSplit::check(Theory::Effort e, QEffort quant_e) in check() argument
89 if (quant_e == QEFFORT_CONFLICT) in check()
|
| H A D | quant_split.h | 42 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | rewrite_engine.h | 54 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | local_theory_ext.h | 72 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | anti_skolem.h | 43 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | local_theory_ext.cpp | 132 void LtePartialInst::check(Theory::Effort e, QEffort quant_e) in check() argument
135 if (quant_e == QEFFORT_CONFLICT && d_needsCheck) in check()
|
| H A D | rewrite_engine.cpp | 73 void RewriteEngine::check(Theory::Effort e, QEffort quant_e) in check() argument
75 if (quant_e == QEFFORT_STANDARD) in check()
|
| H A D | quant_util.h | 92 virtual void check(Theory::Effort e, QEffort quant_e) = 0;
|
| H A D | anti_skolem.cpp | 95 void QuantAntiSkolem::check(Theory::Effort e, QEffort quant_e) in check() argument
97 if (quant_e == QEFFORT_STANDARD) in check()
|
| H A D | instantiate.h | 55 virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e,
|
| H A D | quant_conflict_find.h | 250 void check(Theory::Effort level, QEffort quant_e) override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | model_engine.cpp | 68 void ModelEngine::check(Theory::Effort e, QEffort quant_e) in check() argument
72 doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); in check()
75 doCheck = quant_e == QEFFORT_MODEL; in check()
|
| H A D | model_engine.h | 55 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | bounded_integers.h | 165 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | bounded_integers.cpp | 280 void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) in check() argument
282 if (quant_e != QEFFORT_STANDARD) in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | instantiation_engine.cpp | 114 void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) in check() argument
117 if (quant_e == QEFFORT_STANDARD) in check()
|
| H A D | instantiation_engine.h | 82 void check(Theory::Effort e, QEffort quant_e) override;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.cpp | 631 QuantifiersModule::QEffort quant_e = in check() local
633 d_curr_effort_level = quant_e; in check()
635 if (needsModelE == quant_e) in check()
659 << " at effort " << quant_e << "..." in check()
661 mdl->check(e, quant_e); in check()
675 if (quant_e == QuantifiersModule::QEFFORT_CONFLICT) in check()
688 else if (quant_e == QuantifiersModule::QEFFORT_MODEL) in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_engine.h | 67 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | synth_engine.cpp | 53 void SynthEngine::check(Theory::Effort e, QEffort quant_e) in check() argument
56 if (quant_e != QEFFORT_MODEL) in check()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.h | 73 void check(Theory::Effort e, QEffort quant_e) override;
|
| H A D | inst_strategy_cegqi.cpp | 286 void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) in check() argument
288 if (quant_e == QEFFORT_STANDARD) in check()
|