diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.cpp')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 729dd6100..232499fbf 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -97,13 +97,6 @@ void Instantiate::addRewriter(InstantiationRewriter* ir) } bool Instantiate::addInstantiation( - Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts) -{ - Assert(q[0].getNumChildren() == m.d_vals.size()); - return addInstantiation(q, m.d_vals, mkRep, modEq, doVts); -} - -bool Instantiate::addInstantiation( Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts) { // For resource-limiting (also does a time check). @@ -142,7 +135,7 @@ bool Instantiate::addInstantiation( } #ifdef CVC4_ASSERTIONS bool bad_inst = false; - if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i])) + if (TermUtil::containsUninterpretedConstant(terms[i])) { Trace("inst") << "***& inst contains uninterpreted constant : " << terms[i] << std::endl; @@ -157,7 +150,7 @@ bool Instantiate::addInstantiation( } else if (options::cegqi()) { - Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); + Node icf = TermUtil::getInstConstAttr(terms[i]); if (!icf.isNull()) { if (icf == q) @@ -254,7 +247,7 @@ bool Instantiate::addInstantiation( Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get()); Node orig_body = body; // now preprocess, storing the trust node for the rewrite - TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true); + TrustNode tpBody = QuantifiersRewriter::preprocess(body, true); if (!tpBody.isNull()) { Assert(tpBody.getKind() == TrustNodeKind::REWRITE); @@ -462,13 +455,6 @@ Node Instantiate::getInstantiation(Node q, return body; } -Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts) -{ - Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); - Assert(m.d_vals.size() == q[0].getNumChildren()); - return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts); -} - Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts) { Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); |