diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f756fcfd1..be04f9404 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -25,6 +25,7 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" @@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q, #endif } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* ec = d_treg.getEntailmentCheck(); // Note we check for entailment before checking for term vector duplication. // Although checking for term vector duplication is a faster check, it is // included automatically with recordInstantiationInternal, hence we prefer @@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q, { subs[q[0][i]] = terms[i]; } - if (tdb->isEntailed(q[1], subs, false, true)) + if (ec->isEntailed(q[1], subs, false, true)) { Trace("inst-add-debug") << " --> Currently entailed." << std::endl; ++(d_statistics.d_inst_duplicate_ent); @@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q, // check based on instantiation level if (options::instMaxLevel() != -1) { + TermDb* tdb = d_treg.getTermDatabase(); for (Node& t : terms) { if (!tdb->isTermEligibleForInstantiation(t, q)) @@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // will never succeed with 1 variable return false; } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; // set up information for below std::vector<Node>& vars = d_qreg.d_vars[q]; @@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (options::instNoEntail()) { Trace("inst-exp-fail") << " check entailment" << std::endl; - success = tdb->isEntailed(q[1], subs, false, true); + success = echeck->isEntailed(q[1], subs, false, true); Trace("inst-exp-fail") << " entailed: " << success << std::endl; } // check whether the instantiation rewrites to the same thing |