Infrastructure for instantiation rewriter (#3262)

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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<InstRewriterCegqi> 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<Node>& 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<Node>& 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<InstantiationNotify*> d_inst_notify;
+  /** instantiation rewriter classes */
+  std::vector<InstantiationRewriter*> 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:
   /**