From d278cfe019534f8765a9979c3181ae1f8fbc8470 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Feb 2021 12:16:42 -0600 Subject: [PATCH] Simplify interface to instantiate (#5926) Does not support InstMatch interfaces anymore, which are spurious. --- .../quantifiers/ematching/ho_trigger.cpp | 4 +- .../ematching/inst_match_generator.h | 2 +- .../ematching/inst_match_generator_multi.cpp | 3 +- .../ematching/inst_match_generator_multi.h | 1 + .../ematching/inst_match_generator_simple.cpp | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 2 +- src/theory/quantifiers/fmf/model_engine.cpp | 2 +- src/theory/quantifiers/inst_match_trie.cpp | 133 +++++++------- src/theory/quantifiers/inst_match_trie.h | 163 +++--------------- src/theory/quantifiers/instantiate.cpp | 20 +-- src/theory/quantifiers/instantiate.h | 22 +-- 11 files changed, 107 insertions(+), 247 deletions(-) diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 4c606a273..875c74aa4 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -368,7 +368,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) else { // do not run higher-order matching - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); } } @@ -381,7 +381,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); } else { diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index f03d1cf20..b5c81b766 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -19,7 +19,7 @@ #include #include "expr/node_trie.h" -#include "theory/quantifiers/inst_match_trie.h" +#include "theory/quantifiers/inst_match.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 4f393bc4f..e4fb3fc41 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -191,7 +191,8 @@ void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe, uint64_t& addedLemmas) { // see if these produce new matches - d_children_trie[fromChildIndex].addInstMatch(qe->getState(), d_quant, m); + d_children_trie[fromChildIndex].addInstMatch( + qe->getState(), d_quant, m.d_vals); // possibly only do the following if we know that new matches will be // produced? the issue is that instantiations are filtered in quantifiers // engine, and so there is no guarentee that diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index b68d362cc..2007e652d 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -21,6 +21,7 @@ #include #include "expr/node_trie.h" #include "theory/quantifiers/ematching/inst_match_generator.h" +#include "theory/quantifiers/inst_match_trie.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index b5ef7792d..a46eb12ce 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -140,7 +140,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // we do not need the trigger parent for simple triggers (no post-processing // required) - if (qe->getInstantiate()->addInstantiation(d_quant, m)) + if (qe->getInstantiate()->addInstantiation(d_quant, m.d_vals)) { addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index ac43d3bc9..8d9cfd3a3 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -143,7 +143,7 @@ uint64_t Trigger::addInstantiations() bool Trigger::sendInstantiation(InstMatch& m) { - return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_quant, m.d_vals); } bool Trigger::mkTriggerTerms(Node q, diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 1c0a74013..4ca820709 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -291,7 +291,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if (inst->addInstantiation(f, m, true)) + if (inst->addInstantiation(f, m.d_vals, true)) { addedLemmas++; if (d_qstate.isInConflict()) diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index a42823845..993fad90a 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of inst match class + ** \brief Implementation of inst match trie class **/ #include "theory/quantifiers/inst_match_trie.h" @@ -26,9 +26,19 @@ namespace CVC4 { namespace theory { namespace inst { +bool InstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs, + Node q, + const std::vector& m, + bool modEq, + ImtIndexOrder* imtio, + unsigned index) +{ + return !addInstMatch(qs, q, m, modEq, imtio, true, index); +} + bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, Node f, - std::vector& m, + const std::vector& m, bool modEq, ImtIndexOrder* imtio, bool onlyExist, @@ -84,7 +94,7 @@ bool InstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, } bool InstMatchTrie::removeInstMatch(Node q, - std::vector& m, + const std::vector& m, ImtIndexOrder* imtio, unsigned index) { @@ -108,49 +118,27 @@ bool InstMatchTrie::removeInstMatch(Node q, void InstMatchTrie::print(std::ostream& out, Node q, - std::vector& terms, - bool useActive, - std::vector& active) const + std::vector& terms) const { if (terms.size() == q[0].getNumChildren()) { - bool print; - if (useActive) + out << " ( "; + for (unsigned i = 0, size = terms.size(); i < size; i++) { - if (hasInstLemma()) - { - Node lem = getInstLemma(); - print = std::find(active.begin(), active.end(), lem) != active.end(); - } - else + if (i > 0) { - print = false; + out << ", "; } + out << terms[i]; } - else - { - print = true; - } - if (print) - { - out << " ( "; - for (unsigned i = 0, size = terms.size(); i < size; i++) - { - if (i > 0) - { - out << ", "; - } - out << terms[i]; - } - out << " )" << std::endl; - } + out << " )" << std::endl; } else { for (const std::pair& d : d_data) { terms.push_back(d.first); - d.second.print(out, q, terms, useActive, active); + d.second.print(out, q, terms); terms.pop_back(); } } @@ -182,6 +170,14 @@ void InstMatchTrie::getInstantiations(Node q, } } +void InstMatchTrie::clear() { d_data.clear(); } + +void InstMatchTrie::print(std::ostream& out, Node q) const +{ + std::vector terms; + print(out, q, terms); +} + CDInstMatchTrie::~CDInstMatchTrie() { for (std::pair& d : d_data) @@ -192,9 +188,18 @@ CDInstMatchTrie::~CDInstMatchTrie() d_data.clear(); } +bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs, + Node q, + const std::vector& m, + bool modEq, + unsigned index) +{ + return !addInstMatch(qs, q, m, modEq, index, true); +} + bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, Node f, - std::vector& m, + const std::vector& m, bool modEq, unsigned index, bool onlyExist) @@ -262,7 +267,7 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs, } bool CDInstMatchTrie::removeInstMatch(Node q, - std::vector& m, + const std::vector& m, unsigned index) { if (index == q[0].getNumChildren()) @@ -284,48 +289,26 @@ bool CDInstMatchTrie::removeInstMatch(Node q, void CDInstMatchTrie::print(std::ostream& out, Node q, - std::vector& terms, - bool useActive, - std::vector& active) const + std::vector& terms) const { if (d_valid.get()) { if (terms.size() == q[0].getNumChildren()) { - bool print; - if (useActive) - { - if (hasInstLemma()) - { - Node lem = getInstLemma(); - print = std::find(active.begin(), active.end(), lem) != active.end(); - } - else - { - print = false; - } - } - else - { - print = true; - } - if (print) + out << " ( "; + for (unsigned i = 0; i < terms.size(); i++) { - out << " ( "; - for (unsigned i = 0; i < terms.size(); i++) - { - if (i > 0) out << " "; - out << terms[i]; - } - out << " )" << std::endl; + if (i > 0) out << " "; + out << terms[i]; } + out << " )" << std::endl; } else { for (const std::pair& d : d_data) { terms.push_back(d.first); - d.second->print(out, q, terms, useActive, active); + d.second->print(out, q, terms); terms.pop_back(); } } @@ -362,6 +345,28 @@ void CDInstMatchTrie::getInstantiations(Node q, } } +void CDInstMatchTrie::print(std::ostream& out, Node q) const +{ + std::vector terms; + print(out, q, terms); +} + +bool InstMatchTrieOrdered::addInstMatch(quantifiers::QuantifiersState& qs, + Node q, + const std::vector& m, + bool modEq) +{ + return d_imt.addInstMatch(qs, q, m, modEq, d_imtio); +} + +bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs, + Node q, + const std::vector& m, + bool modEq) +{ + return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio); +} + } /* CVC4::theory::inst namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index c8d0214b6..c45badc38 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief inst match class + ** \brief inst match trie class **/ #include "cvc4_private.h" @@ -22,14 +22,13 @@ #include "context/cdlist.h" #include "context/cdo.h" #include "expr/node.h" -#include "theory/quantifiers/inst_match.h" namespace CVC4 { namespace theory { class QuantifiersEngine; -namespace { +namespace quantifiers { class QuantifiersState; } @@ -65,23 +64,10 @@ class InstMatchTrie */ bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, - InstMatch& m, + const std::vector& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, - unsigned index = 0) - { - return !addInstMatch(qs, q, m, modEq, imtio, true, index); - } - /** exists inst match, vector version */ - bool existsInstMatch(quantifiers::QuantifiersState& qs, - Node q, - std::vector& m, - bool modEq = false, - ImtIndexOrder* imtio = NULL, - unsigned index = 0) - { - return !addInstMatch(qs, q, m, modEq, imtio, true, index); - } + ImtIndexOrder* imtio = nullptr, + unsigned index = 0); /** add inst match * * This method adds (the suffix of) m starting at the given index to this @@ -90,22 +76,11 @@ class InstMatchTrie * If modEq is true, we check for duplication modulo equality the current * equalities in the equality engine of qs. */ - bool addInstMatch(quantifiers::QuantifiersState& qs, - Node q, - InstMatch& m, - bool modEq = false, - ImtIndexOrder* imtio = NULL, - bool onlyExist = false, - unsigned index = 0) - { - return addInstMatch(qs, q, m.d_vals, modEq, imtio, onlyExist, index); - } - /** add inst match, vector version */ bool addInstMatch(quantifiers::QuantifiersState& qs, Node f, - std::vector& m, + const std::vector& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, + ImtIndexOrder* imtio = nullptr, bool onlyExist = false, unsigned index = 0); /** remove inst match @@ -115,8 +90,8 @@ class InstMatchTrie * The domain of m is the bound variables of quantified formula q. */ bool removeInstMatch(Node f, - std::vector& m, - ImtIndexOrder* imtio = NULL, + const std::vector& m, + ImtIndexOrder* imtio = nullptr, unsigned index = 0); /** * Adds the instantiations for q into insts. @@ -124,16 +99,9 @@ class InstMatchTrie void getInstantiations(Node q, std::vector>& insts) const; /** clear the data of this class */ - void clear() { d_data.clear(); } + void clear(); /** print this class */ - void print(std::ostream& out, - Node q, - bool useActive, - std::vector& active) const - { - std::vector terms; - print(out, q, terms, useActive, active); - } + void print(std::ostream& out, Node q) const; /** the data */ std::map d_data; @@ -145,21 +113,7 @@ class InstMatchTrie /** helper for print * terms accumulates the path we are on in the trie. */ - void print(std::ostream& out, - Node q, - std::vector& terms, - bool useActive, - std::vector& active) const; - /** set instantiation lemma at this node in the trie */ - void setInstLemma(Node n) - { - d_data.clear(); - d_data[n].clear(); - } - /** does this node of the trie store an instantiation lemma? */ - bool hasInstLemma() const { return !d_data.empty(); } - /** get the instantiation lemma stored in this node of the trie */ - Node getInstLemma() const { return d_data.begin()->first; } + void print(std::ostream& out, Node q, std::vector& terms) const; }; /** trie for InstMatch objects @@ -183,21 +137,9 @@ class CDInstMatchTrie */ bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, - InstMatch& m, + const std::vector& m, bool modEq = false, - unsigned index = 0) - { - return !addInstMatch(qs, q, m, modEq, index, true); - } - /** exists inst match, vector version */ - bool existsInstMatch(quantifiers::QuantifiersState& qs, - Node q, - std::vector& m, - bool modEq = false, - unsigned index = 0) - { - return !addInstMatch(qs, q, m, modEq, index, true); - } + unsigned index = 0); /** add inst match * * This method adds (the suffix of) m starting at the given index to this @@ -209,17 +151,7 @@ class CDInstMatchTrie */ bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, - InstMatch& m, - bool modEq = false, - unsigned index = 0, - bool onlyExist = false) - { - return addInstMatch(qs, q, m.d_vals, modEq, index, onlyExist); - } - /** add inst match, vector version */ - bool addInstMatch(quantifiers::QuantifiersState& qs, - Node q, - std::vector& m, + const std::vector& m, bool modEq = false, unsigned index = 0, bool onlyExist = false); @@ -229,67 +161,28 @@ class CDInstMatchTrie * It returns true if and only if this entry existed in this trie. * The domain of m is the bound variables of quantified formula q. */ - bool removeInstMatch(Node q, std::vector& m, unsigned index = 0); + bool removeInstMatch(Node q, const std::vector& m, unsigned index = 0); /** * Adds the instantiations for q into insts. */ void getInstantiations(Node q, std::vector>& insts) const; /** print this class */ - void print(std::ostream& out, - Node q, - bool useActive, - std::vector& active) const - { - std::vector terms; - print(out, q, terms, useActive, active); - } + void print(std::ostream& out, Node q) const; private: /** Helper for getInstantiations.*/ void getInstantiations(Node q, std::vector>& insts, std::vector& terms) const; + /** helper for print + * terms accumulates the path we are on in the trie. + */ + void print(std::ostream& out, Node q, std::vector& terms) const; /** the data */ std::map d_data; /** is valid */ context::CDO d_valid; - /** helper for print - * terms accumulates the path we are on in the trie. - */ - void print(std::ostream& out, - Node q, - std::vector& terms, - bool useActive, - std::vector& active) const; - /** helper for get instantiations - * terms accumulates the path we are on in the trie. - */ - void getInstantiations(std::vector& insts, - Node q, - std::vector& terms, - QuantifiersEngine* qe, - bool useActive, - std::vector& active) const; - /** helper for get explanation for inst lemma - * terms accumulates the path we are on in the trie. - */ - void getExplanationForInstLemmas( - Node q, - std::vector& terms, - const std::vector& lems, - std::map& quant, - std::map >& tvec) const; - /** set instantiation lemma at this node in the trie */ - void setInstLemma(Node n) - { - d_data.clear(); - d_data[n] = NULL; - } - /** does this node of the trie store an instantiation lemma? */ - bool hasInstLemma() const { return !d_data.empty(); } - /** get the instantiation lemma stored in this node of the trie */ - Node getInstLemma() const { return d_data.begin()->first; } }; /** inst match trie ordered @@ -314,11 +207,8 @@ class InstMatchTrieOrdered */ bool addInstMatch(quantifiers::QuantifiersState& qs, Node q, - InstMatch& m, - bool modEq = false) - { - return d_imt.addInstMatch(qs, q, m, modEq, d_imtio); - } + const std::vector& m, + bool modEq = false); /** returns true if this trie contains m * * This method returns true if the match m exists in this @@ -327,11 +217,8 @@ class InstMatchTrieOrdered */ bool existsInstMatch(quantifiers::QuantifiersState& qs, Node q, - InstMatch& m, - bool modEq = false) - { - return d_imt.existsInstMatch(qs, q, m, modEq, d_imtio); - } + const std::vector& m, + bool modEq = false); private: /** the ordering */ 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 @@ -96,13 +96,6 @@ void Instantiate::addRewriter(InstantiationRewriter* ir) d_instRewrite.push_back(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& terms, bool mkRep, bool modEq, bool doVts) { @@ -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& terms, bool doVts) { Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end()); diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 4188311ec..c9911785f 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -120,7 +120,7 @@ class Instantiate : public QuantifiersUtil /** do instantiation specified by m * * This function returns true if the instantiation lemma for quantified - * formula q for the substitution specified by m is successfully enqueued + * formula q for the substitution specified by terms is successfully enqueued * via a call to QuantifiersInferenceManager::addPendingLemma. * mkRep : whether to take the representatives of the terms in the range of * the substitution m, @@ -141,26 +141,11 @@ class Instantiate : public QuantifiersUtil * (5) The instantiation lemma is a duplicate of previously added lemma. * */ - bool addInstantiation(Node q, - InstMatch& m, - bool mkRep = false, - bool modEq = false, - bool doVts = false); - /** add instantiation - * - * Same as above, but the substitution we are considering maps the variables - * of q to the vector terms, in order. - */ bool addInstantiation(Node q, std::vector& terms, bool mkRep = false, bool modEq = false, bool doVts = false); - /** remove pending instantiation - * - * Removes the instantiation lemma lem from the instantiation trie. - */ - bool removeInstantiation(Node q, Node lem, std::vector& terms); /** record instantiation * * Explicitly record that q has been instantiated with terms. This is the @@ -194,11 +179,6 @@ class Instantiate : public QuantifiersUtil std::vector& terms, bool doVts = false, LazyCDProof* pf = nullptr); - /** get instantiation - * - * Same as above, but with vars/terms specified by InstMatch m. - */ - Node getInstantiation(Node q, InstMatch& m, bool doVts = false); /** get instantiation * * Same as above but with vars equal to the bound variables of q. -- 2.30.2