Searched refs:getInstantiate (Results 1 – 16 of 16) sorted by last modified time
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 628 d_quantEngine->getInstantiate()->recordInstantiation( in doAddInstantiation()
634 if (d_quantEngine->getInstantiate()->addInstantiation( in doAddInstantiation()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | inst_match_generator.cpp | 1092 if (qe->getInstantiate()->addInstantiation(d_quant, m)) in addInstantiations()
|
| H A D | trigger.cpp | 127 return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); in sendInstantiation()
|
| H A D | ho_trigger.cpp | 373 return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); in sendInstantiation()
386 return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); in sendInstantiation()
|
| H A D | candidate_generator.cpp | 200 return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); in getNextCandidate()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/fmf/ |
| H A D | full_model_check.cpp | 660 if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) in doExhaustiveInstantiation()
804 if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) in exhaustiveInstantiate()
|
| H A D | model_builder.cpp | 122 Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms); in debugModel()
|
| H A D | model_engine.cpp | 288 Instantiate* inst = d_quantEngine->getInstantiate(); in exhaustiveInstantiate()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.cpp | 341 quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const in getInstantiate() function in QuantifiersEngine
|
| H A D | quantifiers_engine.h | 137 quantifiers::Instantiate* getInstantiate() const;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | inst_propagator.cpp | 674 if (!d_qe->getInstantiate()->removeInstantiation( in filterInstantiations()
|
| H A D | inst_strategy_enumerative.cpp | 277 if (d_quantEngine->getInstantiate()->addInstantiation(f, terms)) in process()
|
| H A D | inst_match_trie.cpp | 215 insts.push_back(qe->getInstantiate()->getInstantiation(q, terms, true)); in getInstantiations()
475 qe->getInstantiate()->getInstantiation(q, terms, true)); in getInstantiations()
|
| H A D | quant_conflict_find.cpp | 585 p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms); in isTConstraintSpurious()
2015 Node inst = d_quantEngine->getInstantiate() in check()
2022 if (d_quantEngine->getInstantiate()->addInstantiation( in check()
|
| H A D | rewrite_engine.cpp | 163 if (d_quantEngine->getInstantiate()->addInstantiation(f, inst)) in checkRewriteRule()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_conjecture.cpp | 152 d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( in assign()
|