From 81cd457d729f845f1b76d457359a0ae9963c0f88 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Sep 2019 17:08:07 -0500 Subject: [PATCH] Infrastructure for instantiation rewriter (#3262) --- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 38 +++++++++++++ .../quantifiers/cegqi/inst_strategy_cegqi.h | 53 ++++++++++++++++++- src/theory/quantifiers/instantiate.cpp | 28 ++++------ src/theory/quantifiers/instantiate.h | 32 ++++++++++- src/theory/quantifiers_engine.cpp | 5 +- src/theory/quantifiers_engine.h | 3 -- 6 files changed, 132 insertions(+), 27 deletions(-) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index ac4d05194..7ad7e6996 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -37,8 +37,22 @@ namespace CVC4 { namespace theory { namespace quantifiers { +InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p) + : InstantiationRewriter(), d_parent(p) +{ +} + +Node InstRewriterCegqi::rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) +{ + return d_parent->rewriteInstantiation(q, terms, inst, doVts); +} + InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) : QuantifiersModule(qe), + d_irew(new InstRewriterCegqi(this)), d_cbqi_set_quant_inactive(false), d_incomplete_check(false), d_added_cbqi_lemma(qe->getUserContext()), @@ -436,6 +450,30 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q) } } } +Node InstStrategyCegqi::rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) +{ + if (doVts) + { + // do virtual term substitution + inst = Rewriter::rewrite(inst); + Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl; + inst = d_quantEngine->getTermUtil()->rewriteVtsSymbols(inst); + Trace("quant-vts-debug") << "...got " << inst << std::endl; + } + if (options::cbqiNestedQE()) + { + inst = doNestedQE(q, terms, inst, doVts); + } + return inst; +} + +InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const +{ + return d_irew.get(); +} Node InstStrategyCegqi::doNestedQENode( Node q, Node ceq, Node n, std::vector& inst_terms, bool doVts) diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 32f41e476..f3624d834 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -21,6 +21,7 @@ #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -28,6 +29,31 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class InstStrategyCegqi; + +/** + * An instantiation rewriter based on the counterexample-guided instantiation + * quantifiers module below. + */ +class InstRewriterCegqi : public InstantiationRewriter +{ + public: + InstRewriterCegqi(InstStrategyCegqi* p); + ~InstRewriterCegqi() {} + /** + * Rewrite the instantiation via d_parent, based on virtual term substitution + * and nested quantifier elimination. + */ + Node rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) override; + + private: + /** pointer to the parent of this class */ + InstStrategyCegqi* d_parent; +}; + /** * Counterexample-guided quantifier instantiation module. * @@ -69,8 +95,21 @@ class InstStrategyCegqi : public QuantifiersModule void preRegisterQuantifier(Node q) override; // presolve void presolve() override; - /** Do nested quantifier elimination. */ - Node doNestedQE(Node q, std::vector& inst_terms, Node lem, bool doVts); + + /** + * Rewrite the instantiation inst of quantified formula q for terms; return + * the result. + * + * 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. + */ + Node rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts); + /** get the instantiation rewriter object */ + InstantiationRewriter* getInstRewriter() const; //------------------- interface for CegqiOutputInstStrategy /** Instantiate the current quantified formula forall x. Q with x -> subs. */ @@ -80,6 +119,8 @@ class InstStrategyCegqi : public QuantifiersModule //------------------- end interface for CegqiOutputInstStrategy protected: + /** The instantiation rewriter object */ + std::unique_ptr d_irew; /** set quantified formula inactive * * This flag is set to true during a full effort check if at least one @@ -181,6 +222,14 @@ class InstStrategyCegqi : public QuantifiersModule NodeIntMap d_nested_qe_waitlist_proc; std::map< Node, std::vector< Node > > d_nested_qe_waitlist; + /** Do nested quantifier elimination. + * + * This rewrites the quantified formulas in inst based on nested quantifier + * elimination. In this method, inst is the instantiation of quantified + * formula q for the vector terms. The flag doVts indicates whether we must + * apply virtual term substitution (if terms contains virtual terms). + */ + Node doNestedQE(Node q, std::vector& terms, Node inst, bool doVts); }; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index df23adcdd..ea90ddd66 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -85,6 +85,11 @@ void Instantiate::addNotify(InstantiationNotify* in) d_inst_notify.push_back(in); } +void Instantiate::addRewriter(InstantiationRewriter* ir) +{ + d_instRewrite.push_back(ir); +} + void Instantiate::notifyFlushLemmas() { for (InstantiationNotify*& in : d_inst_notify) @@ -244,14 +249,7 @@ bool Instantiate::addInstantiation( // get the instantiation Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts); Node orig_body = body; - if (options::cbqiNestedQE()) - { - InstStrategyCegqi* icegqi = d_qe->getInstStrategyCegqi(); - if (icegqi) - { - body = icegqi->doNestedQE(q, terms, body, doVts); - } - } + // now preprocess body = quantifiers::QuantifiersRewriter::preprocess(body, true); Trace("inst-debug") << "...preprocess to " << body << std::endl; @@ -413,17 +411,13 @@ Node Instantiate::getInstantiation(Node q, Node body; Assert(vars.size() == terms.size()); Assert(q[0].getNumChildren() == vars.size()); - // TODO (#1386) : optimize this + // 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()); - if (doVts) + // run rewriters to rewrite the instantiation in sequence. + for (InstantiationRewriter*& ir : d_instRewrite) { - // do virtual term substitution - body = Rewriter::rewrite(body); - Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; - Node body_r = d_term_util->rewriteVtsSymbols(body); - Trace("quant-vts-debug") << " ...result: " << body_r - << std::endl; - body = body_r; + body = ir->rewriteInstantiation(q, terms, body, doVts); } return body; } diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 769ae4ea3..4936693d1 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -69,6 +69,32 @@ class InstantiationNotify virtual void filterInstantiations() = 0; }; +/** Instantiation rewriter + * + * This class is used for cases where instantiation lemmas can be rewritten by + * external utilities. Examples of this include virtual term substitution and + * nested quantifier elimination techniques. + */ +class InstantiationRewriter +{ + public: + InstantiationRewriter() {} + virtual ~InstantiationRewriter() {} + + /** rewrite instantiation + * + * The node inst is the instantiation of quantified formula q for terms. + * This method returns the rewritten form of the instantiation. + * + * The flag doVts is whether we must apply virtual term substitution to the + * instantiation. + */ + virtual Node rewriteInstantiation(Node q, + std::vector& terms, + Node inst, + bool doVts) = 0; +}; + /** Instantiate * * This class is used for generating instantiation lemmas. It maintains an @@ -103,7 +129,7 @@ class Instantiate : public QuantifiersUtil /** check incomplete */ bool checkComplete() override; - //--------------------------------------notify objects + //--------------------------------------notify/rewrite objects /** add instantiation notify * * Adds an instantiation notify class to listen to the instantiations reported @@ -112,6 +138,8 @@ class Instantiate : public QuantifiersUtil void addNotify(InstantiationNotify* in); /** get number of instantiation notify added to this class */ bool hasNotify() const { return !d_inst_notify.empty(); } + /** add instantiation rewriter */ + void addRewriter(InstantiationRewriter* ir); /** notify flush lemmas * * This is called just before the quantifiers engine flushes its lemmas to @@ -342,6 +370,8 @@ class Instantiate : public QuantifiersUtil TermUtil* d_term_util; /** instantiation notify classes */ std::vector d_inst_notify; + /** instantiation rewriter classes */ + std::vector d_instRewrite; /** statistics for debugging total instantiation */ int d_total_inst_count_debug; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index f57667be5..def1f969c 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -128,6 +128,7 @@ class QuantifiersEnginePrivate { d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe)); modules.push_back(d_i_cbqi.get()); + qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter()); } if (options::ceGuidedInst()) { @@ -391,10 +392,6 @@ quantifiers::SynthEngine* QuantifiersEngine::getSynthEngine() const { return d_private->d_synth_e.get(); } -quantifiers::InstStrategyCegqi* QuantifiersEngine::getInstStrategyCegqi() const -{ - return d_private->d_i_cbqi.get(); -} QuantifiersModule * QuantifiersEngine::getOwner( Node q ) { std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1f8c13f7b..458ba07bc 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" @@ -119,8 +118,6 @@ public: quantifiers::BoundedIntegers* getBoundedIntegers() const; /** ceg instantiation */ quantifiers::SynthEngine* getSynthEngine() const; - /** get inst strategy cbqi */ - quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; //---------------------- end modules private: /** -- 2.30.2