From 5f3d21a7402538af837eaf943b5252b1db90080b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Sep 2020 19:47:52 -0500 Subject: [PATCH] (proof-new) Support proofs of quantifier instantiation (#5001) This adds basic support for proofs of quantifier instantiation, which is the main method for sending lemmas from TheoryQuantifiers. Quantifier instantiation is also heavily used for solving extended string functions. --- .../passes/quantifiers_preprocess.cpp | 5 +- src/preprocessing/passes/sygus_inference.cpp | 7 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 24 ++- .../quantifiers/cegqi/inst_strategy_cegqi.h | 22 +- src/theory/quantifiers/instantiate.cpp | 130 ++++++++++- src/theory/quantifiers/instantiate.h | 32 ++- .../quantifiers/quantifiers_rewriter.cpp | 7 +- src/theory/quantifiers/quantifiers_rewriter.h | 5 +- src/theory/quantifiers_engine.cpp | 38 +++- src/theory/quantifiers_engine.h | 204 ++++++++++-------- src/theory/theory_engine.cpp | 3 +- 11 files changed, 337 insertions(+), 140 deletions(-) diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 3052e9629..cda7ad67a 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -39,9 +39,10 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal( for (size_t i = 0; i < size; ++i) { Node prev = (*assertionsToPreprocess)[i]; - Node next = quantifiers::QuantifiersRewriter::preprocess(prev); - if (next != prev) + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(prev); + if (!trn.isNull()) { + Node next = trn.getNode(); assertionsToPreprocess->replace(i, Rewriter::rewrite(next)); Trace("quantifiers-preprocess") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-preprocess") diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d44321a35..82515c6a4 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -24,6 +24,7 @@ using namespace std; using namespace CVC4::kind; +using namespace CVC4::theory; namespace CVC4 { namespace preprocessing { @@ -135,7 +136,11 @@ bool SygusInference::solveSygus(std::vector& assertions, if (pas.getKind() == FORALL) { // preprocess the quantified formula - pas = theory::quantifiers::QuantifiersRewriter::preprocess(pas); + TrustNode trn = quantifiers::QuantifiersRewriter::preprocess(pas); + if (!trn.isNull()) + { + pas = trn.getNode(); + } Trace("sygus-infer-debug") << " ...preprocessed to " << pas << std::endl; } if (pas.getKind() == FORALL) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index c156cbdf8..a771309f0 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -42,10 +42,10 @@ InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p) { } -Node InstRewriterCegqi::rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) +TrustNode InstRewriterCegqi::rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) { return d_parent->rewriteInstantiation(q, terms, inst, doVts); } @@ -453,11 +453,12 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q) } } } -Node InstStrategyCegqi::rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) +TrustNode InstStrategyCegqi::rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) { + Node prevInst = inst; if (doVts) { // do virtual term substitution @@ -470,7 +471,12 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q, { inst = doNestedQE(q, terms, inst, doVts); } - return inst; + if (prevInst != inst) + { + // not proof producing yet + return TrustNode::mkTrustRewrite(prevInst, inst, nullptr); + } + return TrustNode::null(); } InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index dac5a198c..c767b8a4e 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -43,12 +43,13 @@ class InstRewriterCegqi : public InstantiationRewriter ~InstRewriterCegqi() {} /** * Rewrite the instantiation via d_parent, based on virtual term substitution - * and nested quantifier elimination. + * and nested quantifier elimination. Returns a TrustNode of kind REWRITE, + * corresponding to the rewrite and its proof generator. */ - Node rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) override; + TrustNode rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) override; private: /** pointer to the parent of this class */ @@ -106,11 +107,14 @@ class InstStrategyCegqi : public QuantifiersModule * We rewrite inst based on virtual term substitution and nested quantifier * elimination. For details, see "Solving Quantified Linear Arithmetic via * Counterexample-Guided Instantiation" FMSD 2017, Reynolds et al. + * + * Returns a TrustNode of kind REWRITE, corresponding to the rewrite and its + * proof generator. */ - Node rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts); + TrustNode rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts); /** get the instantiation rewriter object */ InstantiationRewriter* getInstRewriter() const; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 04b6e0dda..abf2ecdbe 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -35,12 +35,16 @@ namespace CVC4 { namespace theory { namespace quantifiers { -Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u) +Instantiate::Instantiate(QuantifiersEngine* qe, + context::UserContext* u, + ProofNodeManager* pnm) : d_qe(qe), + d_pnm(pnm), d_term_db(nullptr), d_term_util(nullptr), d_total_inst_debug(u), - d_c_inst_match_trie_dom(u) + d_c_inst_match_trie_dom(u), + d_pfInst(pnm ? new CDProof(pnm) : nullptr) { } @@ -231,24 +235,101 @@ bool Instantiate::addInstantiation( return false; } + // Set up a proof if proofs are enabled. This proof stores a proof of + // the instantiation body with q as a free assumption. + std::shared_ptr pfTmp; + if (isProofEnabled()) + { + pfTmp.reset(new LazyCDProof( + d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp")); + } + // construct the instantiation Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; Assert(d_term_util->d_vars[q].size() == terms.size()); // get the instantiation - Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts); + Node body = + getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get()); Node orig_body = body; - // now preprocess - body = quantifiers::QuantifiersRewriter::preprocess(body, true); + // now preprocess, storing the trust node for the rewrite + TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true); + if (!tpBody.isNull()) + { + Assert(tpBody.getKind() == TrustNodeKind::REWRITE); + body = tpBody.getNode(); + // do a tranformation step + if (pfTmp != nullptr) + { + // ----------------- from preprocess + // orig_body orig_body = body + // ------------------------------ EQ_RESOLVE + // body + Node proven = tpBody.getProven(); + // add the transformation proof, or THEORY_PREPROCESS if none provided + pfTmp->addLazyStep(proven, + tpBody.getGenerator(), + true, + "Instantiate::getInstantiation:qpreprocess", + false, + PfRule::THEORY_PREPROCESS); + pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {body}); + } + } Trace("inst-debug") << "...preprocess to " << body << std::endl; // construct the lemma Trace("inst-assert") << "(assert " << body << ")" << std::endl; - Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body); - lem = Rewriter::rewrite(lem); + // construct the instantiation, and rewrite the lemma + Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, q, body); + + // If proofs are enabled, construct the proof, which is of the form: + // ... free assumption q ... + // ------------------------- from pfTmp + // body + // ------------------------- SCOPE + // (=> q body) + // -------------------------- MACRO_SR_PRED_ELIM + // lem + bool hasProof = false; + if (isProofEnabled()) + { + // make the proof of body + std::shared_ptr pfn = pfTmp->getProofFor(body); + // make the scope proof to get (=> q body) + std::vector assumps; + assumps.push_back(q); + std::shared_ptr pfns = d_pnm->mkScope({pfn}, assumps); + Assert(assumps.size() == 1 && assumps[0] == q); + // store in the main proof + d_pfInst->addProof(pfns); + Node prevLem = lem; + lem = Rewriter::rewrite(lem); + if (prevLem != lem) + { + d_pfInst->addStep(lem, PfRule::MACRO_SR_PRED_ELIM, {prevLem}, {}); + } + hasProof = true; + } + else + { + lem = Rewriter::rewrite(lem); + } - // check for lemma duplication - if (!d_qe->addLemma(lem, true, false)) + // added lemma, which checks for lemma duplication + bool addedLem = false; + if (hasProof) + { + // use trust interface + TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get()); + addedLem = d_qe->addTrustedLemma(tlem, true, false); + } + else + { + addedLem = d_qe->addLemma(lem, true, false); + } + + if (!addedLem) { Trace("inst-add-debug") << " --> Lemma already exists." << std::endl; ++(d_statistics.d_inst_duplicate); @@ -367,7 +448,8 @@ bool Instantiate::existsInstantiation(Node q, Node Instantiate::getInstantiation(Node q, std::vector& vars, std::vector& terms, - bool doVts) + bool doVts, + LazyCDProof* pf) { Node body; Assert(vars.size() == terms.size()); @@ -375,10 +457,34 @@ Node Instantiate::getInstantiation(Node q, // Notice that this could be optimized, but no significant performance // improvements were observed with alternative implementations (see #1386). body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end()); + + // store the proof of the instantiated body, with (open) assumption q + if (pf != nullptr) + { + pf->addStep(body, PfRule::INSTANTIATE, {q}, terms); + } + // run rewriters to rewrite the instantiation in sequence. for (InstantiationRewriter*& ir : d_instRewrite) { - body = ir->rewriteInstantiation(q, terms, body, doVts); + TrustNode trn = ir->rewriteInstantiation(q, terms, body, doVts); + if (!trn.isNull()) + { + Node newBody = trn.getNode(); + // if using proofs, we store a preprocess + transformation step. + if (pf != nullptr) + { + Node proven = trn.getProven(); + pf->addLazyStep(proven, + trn.getGenerator(), + true, + "Instantiate::getInstantiation:rewrite_inst", + false, + PfRule::THEORY_PREPROCESS); + pf->addStep(newBody, PfRule::EQ_RESOLVE, {body, proven}, {}); + } + body = newBody; + } } return body; } @@ -675,6 +781,8 @@ void Instantiate::getExplanationForInstLemmas( #endif } +bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } + void Instantiate::getInstantiations(std::map >& insts) { if (!options::trackInstLemmas()) diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 8b1e0f7fc..7e984b116 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -20,6 +20,7 @@ #include #include "expr/node.h" +#include "expr/proof.h" #include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -53,11 +54,14 @@ class InstantiationRewriter * * The flag doVts is whether we must apply virtual term substitution to the * instantiation. + * + * Returns a TrustNode of kind REWRITE, corresponding to the rewrite of inst + * and its proof generator. */ - virtual Node rewriteInstantiation(Node q, - std::vector& terms, - Node inst, - bool doVts) = 0; + virtual TrustNode rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) = 0; }; /** Instantiate @@ -84,7 +88,9 @@ class Instantiate : public QuantifiersUtil typedef context::CDHashMap NodeUIntMap; public: - Instantiate(QuantifiersEngine* qe, context::UserContext* u); + Instantiate(QuantifiersEngine* qe, + context::UserContext* u, + ProofNodeManager* pnm = nullptr); ~Instantiate(); /** reset */ @@ -174,11 +180,16 @@ class Instantiate : public QuantifiersUtil * * Returns the instantiation lemma for q under substitution { vars -> terms }. * doVts is whether to apply virtual term substitution to its body. + * + * If provided, pf is a lazy proof for which we store a proof of the + * returned formula with free assumption q. This typically stores a + * single INSTANTIATE step concluding the instantiated body of q from q. */ Node getInstantiation(Node q, std::vector& vars, std::vector& terms, - bool doVts = false); + bool doVts = false, + LazyCDProof* pf = nullptr); /** get instantiation * * Same as above, but with vars/terms specified by InstMatch m. @@ -277,6 +288,9 @@ class Instantiate : public QuantifiersUtil std::map >& tvec); //--------------------------------------end user-level interface utilities + /** Are proofs enabled for this object? */ + bool isProofEnabled() const; + /** statistics class * * This tracks statistics on the number of instantiations successfully @@ -327,6 +341,8 @@ class Instantiate : public QuantifiersUtil /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; + /** pointer to the proof node manager */ + ProofNodeManager* d_pnm; /** cache of term database for quantifiers engine */ TermDb* d_term_db; /** cache of term util for quantifiers engine */ @@ -359,6 +375,10 @@ class Instantiate : public QuantifiersUtil * of these instantiations, for each quantified formula. */ std::vector > > d_recorded_inst; + /** + * A CDProof storing instantiation steps. + */ + std::unique_ptr d_pfInst; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0848032f8..e34c1c823 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -2052,8 +2052,8 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v return n; } - -Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { +TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst) +{ Node prev = n; if( options::preSkolemQuant() ){ @@ -2078,8 +2078,9 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) { if( n!=prev ){ Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl; Trace("quantifiers-preprocess") << "..returned " << n << std::endl; + return TrustNode::mkTrustRewrite(prev, n, nullptr); } - return n; + return TrustNode::null(); } }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index da3bd2212..196e4b108 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #include "theory/theory_rewriter.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { @@ -284,8 +285,10 @@ public: * registered quantified formula. If this flag is true, we do not apply * certain steps like pre-skolemization since we know they will have no * effect. + * + * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE. */ - static Node preprocess( Node n, bool isInst = false ); + static TrustNode preprocess(Node n, bool isInst = false); static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static Node mkForall( std::vector< Node >& args, Node body, bool marked = false ); static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2e69080e7..da60561ad 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -174,7 +174,8 @@ class QuantifiersEnginePrivate QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, - TheoryEngine* te) + TheoryEngine* te, + ProofNodeManager* pnm) : d_te(te), d_masterEqualityEngine(nullptr), d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)), @@ -187,7 +188,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_term_db(new quantifiers::TermDb(c, u, this)), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes(this)), - d_instantiate(new quantifiers::Instantiate(this, u)), + d_instantiate(new quantifiers::Instantiate(this, u, pnm)), d_skolemize(new quantifiers::Skolemize(this, u)), d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(c, false), @@ -1021,6 +1022,19 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ } } +bool QuantifiersEngine::addTrustedLemma(TrustNode tlem, + bool doCache, + bool doRewrite) +{ + Node lem = tlem.getProven(); + if (!addLemma(lem, doCache, doRewrite)) + { + return false; + } + d_lemmasWaitingPg[lem] = tlem.getGenerator(); + return true; +} + bool QuantifiersEngine::removeLemma( Node lem ) { std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem ); if( it!=d_lemmas_waiting.end() ){ @@ -1102,19 +1116,31 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode() } void QuantifiersEngine::flushLemmas(){ + OutputChannel& out = getOutputChannel(); if( !d_lemmas_waiting.empty() ){ //take default output channel if none is provided d_hasAddedLemma = true; - for( unsigned i=0; i::iterator itp; + for (const Node& lemw : d_lemmas_waiting) + { + Trace("qe-lemma") << "Lemma : " << lemw << std::endl; + itp = d_lemmasWaitingPg.find(lemw); + if (itp != d_lemmasWaitingPg.end()) + { + TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second); + out.trustedLemma(tlemw, LemmaProperty::PREPROCESS); + } + else + { + out.lemma(lemw, LemmaProperty::PREPROCESS); + } } d_lemmas_waiting.clear(); } if( !d_phase_req_waiting.empty() ){ for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){ Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl; - getOutputChannel().requirePhase( it->first, it->second ); + out.requirePhase(it->first, it->second); } d_phase_req_waiting.clear(); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 6afc4f925..bd88034cb 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -55,8 +55,11 @@ class QuantifiersEngine { typedef context::CDList BoolList; typedef context::CDHashSet NodeSet; -public: - QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); + public: + QuantifiersEngine(context::Context* c, + context::UserContext* u, + TheoryEngine* te, + ProofNodeManager* pnm); ~QuantifiersEngine(); //---------------------- external interface /** get theory engine */ @@ -196,100 +199,117 @@ private: void flushLemmas(); public: - /** add lemma lem */ - bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); - /** remove pending lemma */ - bool removeLemma( Node lem ); - /** add require phase */ - void addRequirePhase( Node lit, bool req ); - /** mark relevant quantified formula, this will indicate it should be checked before the others */ - void markRelevant( Node q ); - /** has added lemma */ - bool hasAddedLemma() const; - /** theory engine needs check - * - * This is true if the theory engine has more constraints to process. When - * it is false, we are tentatively going to terminate solving with - * sat/unknown. For details, see TheoryEngine::needCheck. - */ - bool theoryEngineNeedsCheck() const; - /** is in conflict */ - bool inConflict() { return d_conflict; } - /** set conflict */ - void setConflict(); - /** get current q effort */ - QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } - /** get number of waiting lemmas */ - unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } - /** get needs check */ - bool getInstWhenNeedsCheck( Theory::Effort e ); - /** get user pat mode */ - options::UserPatMode getInstUserPatMode(); + /** + * Add lemma to the lemma buffer of this quantifiers engine. + * @param lem The lemma to send + * @param doCache Whether to cache the lemma (to check for duplicate lemmas) + * @param doRewrite Whether to rewrite the lemma + * @return true if the lemma was successfully added to the buffer + */ + bool addLemma(Node lem, bool doCache = true, bool doRewrite = true); + /** + * Add trusted lemma lem, same as above, but where a proof generator may be + * provided along with the lemma. + */ + bool addTrustedLemma(TrustNode tlem, + bool doCache = true, + bool doRewrite = true); + /** remove pending lemma */ + bool removeLemma(Node lem); + /** add require phase */ + void addRequirePhase(Node lit, bool req); + /** mark relevant quantified formula, this will indicate it should be checked + * before the others */ + void markRelevant(Node q); + /** has added lemma */ + bool hasAddedLemma() const; + /** theory engine needs check + * + * This is true if the theory engine has more constraints to process. When + * it is false, we are tentatively going to terminate solving with + * sat/unknown. For details, see TheoryEngine::needCheck. + */ + bool theoryEngineNeedsCheck() const; + /** is in conflict */ + bool inConflict() { return d_conflict; } + /** set conflict */ + void setConflict(); + /** get current q effort */ + QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } + /** get number of waiting lemmas */ + unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } + /** get needs check */ + bool getInstWhenNeedsCheck(Theory::Effort e); + /** get user pat mode */ + options::UserPatMode getInstUserPatMode(); - public: - /** add term to database */ - void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false ); - /** notification when master equality engine is updated */ - void eqNotifyNewClass(TNode t); - /** debug print equality engine */ - void debugPrintEqualityEngine( const char * c ); - /** get internal representative - * - * Choose a term that is equivalent to a in the current context that is the - * best term for instantiating the index^th variable of quantified formula q. - * If no legal term can be found, we return null. This can occur if: - * - a's type is not a subtype of the type of the index^th variable of q, - * - a is in an equivalent class with all terms that are restricted not to - * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample - * guided instantiation. - */ - Node getInternalRepresentative( Node a, Node q, int index ); +public: + /** add term to database */ + void addTermToDatabase(Node n, + bool withinQuant = false, + bool withinInstClosure = false); + /** notification when master equality engine is updated */ + void eqNotifyNewClass(TNode t); + /** debug print equality engine */ + void debugPrintEqualityEngine(const char* c); + /** get internal representative + * + * Choose a term that is equivalent to a in the current context that is the + * best term for instantiating the index^th variable of quantified formula q. + * If no legal term can be found, we return null. This can occur if: + * - a's type is not a subtype of the type of the index^th variable of q, + * - a is in an equivalent class with all terms that are restricted not to + * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample + * guided instantiation. + */ + Node getInternalRepresentative(Node a, Node q, int index); - public: - //----------user interface for instantiations (see quantifiers/instantiate.h) - /** print instantiations */ - void printInstantiations(std::ostream& out); - /** print solution for synthesis conjectures */ - void printSynthSolution(std::ostream& out); - /** get list of quantified formulas that were instantiated */ - void getInstantiatedQuantifiedFormulas(std::vector& qs); - /** get instantiations */ - void getInstantiations(Node q, std::vector& insts); - void getInstantiations(std::map >& insts); - /** get instantiation term vectors */ - void getInstantiationTermVectors(Node q, - std::vector >& tvecs); - void getInstantiationTermVectors( - std::map > >& insts); - /** get instantiated conjunction */ - Node getInstantiatedConjunction(Node q); - /** get unsat core lemmas */ - bool getUnsatCoreLemmas(std::vector& active_lemmas); - /** get explanation for instantiation lemmas */ - void getExplanationForInstLemmas(const std::vector& lems, - std::map& quant, - std::map >& tvec); +public: + //----------user interface for instantiations (see quantifiers/instantiate.h) + /** print instantiations */ + void printInstantiations(std::ostream& out); + /** print solution for synthesis conjectures */ + void printSynthSolution(std::ostream& out); + /** get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas(std::vector& qs); + /** get instantiations */ + void getInstantiations(Node q, std::vector& insts); + void getInstantiations(std::map >& insts); + /** get instantiation term vectors */ + void getInstantiationTermVectors(Node q, + std::vector >& tvecs); + void getInstantiationTermVectors( + std::map > >& insts); + /** get instantiated conjunction */ + Node getInstantiatedConjunction(Node q); + /** get unsat core lemmas */ + bool getUnsatCoreLemmas(std::vector& active_lemmas); + /** get explanation for instantiation lemmas */ + void getExplanationForInstLemmas(const std::vector& lems, + std::map& quant, + std::map >& tvec); - /** get synth solutions - * - * This method returns true if there is a synthesis solution available. This - * is the case if the last call to check satisfiability originated in a - * check-synth call, and the synthesis engine module of this class - * successfully found a solution for all active synthesis conjectures. - * - * This method adds entries to sol_map that map functions-to-synthesize with - * their solutions, for all active conjectures. This should be called - * immediately after the solver answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * SynthConjecture::getSynthSolutions. - */ - bool getSynthSolutions(std::map >& sol_map); + /** get synth solutions + * + * This method returns true if there is a synthesis solution available. This + * is the case if the last call to check satisfiability originated in a + * check-synth call, and the synthesis engine module of this class + * successfully found a solution for all active synthesis conjectures. + * + * This method adds entries to sol_map that map functions-to-synthesize with + * their solutions, for all active conjectures. This should be called + * immediately after the solver answers unsat for sygus input. + * + * For details on what is added to sol_map, see + * SynthConjecture::getSynthSolutions. + */ + bool getSynthSolutions(std::map >& sol_map); - //----------end user interface for instantiations + //----------end user interface for instantiations - /** statistics class */ - class Statistics { + /** statistics class */ + class Statistics + { public: TimerStat d_time; TimerStat d_qcf_time; @@ -379,6 +399,8 @@ public: BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector d_lemmas_waiting; + /** map from waiting lemmas to their proof generators */ + std::map d_lemmasWaitingPg; /** phase requirements waiting */ std::map d_phase_req_waiting; /** inst round counters TODO: make context-dependent? */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6837d4be5..6a548e5b6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -165,7 +165,8 @@ void TheoryEngine::finishInit() { if (d_logicInfo.isQuantified()) { // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + d_quantEngine = + new QuantifiersEngine(d_context, d_userContext, this, d_pnm); } // initialize the theory combination manager, which decides and allocates the // equality engines to use for all theories. -- 2.30.2