Wait to do sygus qe preprocess until full effort check (#2282)

2 files changed, 165 insertions, 121 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 919a8f008..378c2f1d7 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -52,6 +52,19 @@ QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
 
 void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
 {
+  // if we are waiting to assign the conjecture, do it now
+  if (!d_waiting_conj.isNull())
+  {
+    Node q = d_waiting_conj;
+    d_waiting_conj = Node::null();
+    if (!d_conj->isAssigned())
+    {
+      if (!assignConjecture(q))
+      {
+        return;
+      }
+    }
+  }
   unsigned echeck =
       d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
   if( quant_e==echeck ){
@@ -79,134 +92,152 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
   }
 }
 
-void CegInstantiation::registerQuantifier( Node q ) {
-  if( d_quantEngine->getOwner( q )==this ){ // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
-    if( !d_conj->isAssigned() ){
-      Trace("cegqi") << "Register conjecture : " << q << std::endl;
-      Node conj = q;
-      if (options::sygusQePreproc())
+bool CegInstantiation::assignConjecture(Node q)
+{
+  if (d_conj->isAssigned())
+  {
+    return false;
+  }
+  if (options::sygusQePreproc())
+  {
+    // the following does quantifier elimination as a preprocess step
+    // for "non-ground single invocation synthesis conjectures":
+    //   exists f. forall xy. P[ f(x), x, y ]
+    // We run quantifier elimination:
+    //   exists y. P[ z, x, y ] ----> Q[ z, x ]
+    // Where we replace the original conjecture with:
+    //   exists f. forall x. Q[ f(x), x ]
+    // For more details, see Example 6 of Reynolds et al. SYNT 2017.
+    Node body = q[1];
+    if (body.getKind() == NOT && body[0].getKind() == FORALL)
+    {
+      body = body[0][1];
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
+                       << std::endl;
+    quantifiers::SingleInvocationPartition sip;
+    std::vector<Node> funcs;
+    funcs.insert(funcs.end(), q[0].begin(), q[0].end());
+    sip.init(funcs, body);
+    Trace("cegqi-qep") << "...finished, got:" << std::endl;
+    sip.debugPrint("cegqi-qep");
+
+    if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
+    {
+      // create new smt engine to do quantifier elimination
+      SmtEngine smt_qe(nm->toExprManager());
+      smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
+      Trace("cegqi-qep") << "Property is non-ground single invocation, run "
+                            "QE to obtain single invocation."
+                         << std::endl;
+      // partition variables
+      std::vector<Node> all_vars;
+      sip.getAllVariables(all_vars);
+      std::vector<Node> si_vars;
+      sip.getSingleInvocationVariables(si_vars);
+      std::vector<Node> qe_vars;
+      std::vector<Node> nqe_vars;
+      for (unsigned i = 0, size = all_vars.size(); i < size; i++)
       {
-        // the following does quantifier elimination as a preprocess step
-        // for "non-ground single invocation synthesis conjectures":
-        //   exists f. forall xy. P[ f(x), x, y ]
-        // We run quantifier elimination:
-        //   exists y. P[ z, x, y ] ----> Q[ z, x ]
-        // Where we replace the original conjecture with:
-        //   exists f. forall x. Q[ f(x), x ]
-        // For more details, see Example 6 of Reynolds et al. SYNT 2017.
-        Node body = q[1];
-        if (body.getKind() == NOT && body[0].getKind() == FORALL)
+        Node v = all_vars[i];
+        if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
         {
-          body = body[0][1];
+          qe_vars.push_back(v);
         }
-        NodeManager* nm = NodeManager::currentNM();
-        Trace("cegqi-qep") << "Compute single invocation for " << conj << "..."
+        else
+        {
+          nqe_vars.push_back(v);
+        }
+      }
+      std::vector<Node> orig;
+      std::vector<Node> subs;
+      // skolemize non-qe variables
+      for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
+      {
+        Node k = nm->mkSkolem(
+            "k", nqe_vars[i].getType(), "qe for non-ground single invocation");
+        orig.push_back(nqe_vars[i]);
+        subs.push_back(k);
+        Trace("cegqi-qep") << "  subs : " << nqe_vars[i] << " -> " << k
                            << std::endl;
-        quantifiers::SingleInvocationPartition sip;
-        std::vector<Node> funcs;
-        funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
-        sip.init(funcs, body);
-        Trace("cegqi-qep") << "...finished, got:" << std::endl;
-        sip.debugPrint("cegqi-qep");
+      }
+      std::vector<Node> funcs;
+      sip.getFunctions(funcs);
+      for (unsigned i = 0, size = funcs.size(); i < size; i++)
+      {
+        Node f = funcs[i];
+        Node fi = sip.getFunctionInvocationFor(f);
+        Node fv = sip.getFirstOrderVariableForFunction(f);
+        Assert(!fi.isNull());
+        orig.push_back(fi);
+        Node k =
+            nm->mkSkolem("k",
+                         fv.getType(),
+                         "qe for function in non-ground single invocation");
+        subs.push_back(k);
+        Trace("cegqi-qep") << "  subs : " << fi << " -> " << k << std::endl;
+      }
+      Node conj_se_ngsi = sip.getFullSpecification();
+      Trace("cegqi-qep") << "Full specification is " << conj_se_ngsi
+                         << std::endl;
+      Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
+          orig.begin(), orig.end(), subs.begin(), subs.end());
+      Assert(!qe_vars.empty());
+      conj_se_ngsi_subs = nm->mkNode(EXISTS,
+                                     nm->mkNode(BOUND_VAR_LIST, qe_vars),
+                                     conj_se_ngsi_subs.negate());
 
-        if (!sip.isPurelySingleInvocation()
-            && sip.isNonGroundSingleInvocation())
-        {
-          // create new smt engine to do quantifier elimination
-          SmtEngine smt_qe(nm->toExprManager());
-          smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
-          Trace("cegqi-qep") << "Property is non-ground single invocation, run "
-                                "QE to obtain single invocation."
-                             << std::endl;
-          // partition variables
-          std::vector<Node> all_vars;
-          sip.getAllVariables(all_vars);
-          std::vector<Node> si_vars;
-          sip.getSingleInvocationVariables(si_vars);
-          std::vector<Node> qe_vars;
-          std::vector<Node> nqe_vars;
-          for (unsigned i = 0, size = all_vars.size(); i < size; i++)
-          {
-            Node v = all_vars[i];
-            if (std::find(si_vars.begin(), si_vars.end(), v) == si_vars.end())
-            {
-              qe_vars.push_back(v);
-            }
-            else
-            {
-              nqe_vars.push_back(v);
-            }
-          }
-          std::vector<Node> orig;
-          std::vector<Node> subs;
-          // skolemize non-qe variables
-          for (unsigned i = 0, size = nqe_vars.size(); i < size; i++)
-          {
-            Node k = nm->mkSkolem("k",
-                                  nqe_vars[i].getType(),
-                                  "qe for non-ground single invocation");
-            orig.push_back(nqe_vars[i]);
-            subs.push_back(k);
-            Trace("cegqi-qep")
-                << "  subs : " << nqe_vars[i] << " -> " << k << std::endl;
-          }
-          std::vector<Node> funcs;
-          sip.getFunctions(funcs);
-          for (unsigned i = 0, size = funcs.size(); i < size; i++)
-          {
-            Node f = funcs[i];
-            Node fi = sip.getFunctionInvocationFor(f);
-            Node fv = sip.getFirstOrderVariableForFunction(f);
-            Assert(!fi.isNull());
-            orig.push_back(fi);
-            Node k =
-                nm->mkSkolem("k",
-                             fv.getType(),
-                             "qe for function in non-ground single invocation");
-            subs.push_back(k);
-            Trace("cegqi-qep") << "  subs : " << fi << " -> " << k << std::endl;
-          }
-          Node conj_se_ngsi = sip.getFullSpecification();
-          Trace("cegqi-qep")
-              << "Full specification is " << conj_se_ngsi << std::endl;
-          Node conj_se_ngsi_subs = conj_se_ngsi.substitute(
-              orig.begin(), orig.end(), subs.begin(), subs.end());
-          Assert(!qe_vars.empty());
-          conj_se_ngsi_subs = nm->mkNode(EXISTS,
-                                         nm->mkNode(BOUND_VAR_LIST, qe_vars),
-                                         conj_se_ngsi_subs.negate());
+      Trace("cegqi-qep") << "Run quantifier elimination on "
+                         << conj_se_ngsi_subs << std::endl;
+      Expr qe_res = smt_qe.doQuantifierElimination(
+          conj_se_ngsi_subs.toExpr(), true, false);
+      Trace("cegqi-qep") << "Result : " << qe_res << std::endl;
 
-          Trace("cegqi-qep") << "Run quantifier elimination on "
-                             << conj_se_ngsi_subs << std::endl;
-          Expr qe_res = smt_qe.doQuantifierElimination(
-              conj_se_ngsi_subs.toExpr(), true, false);
-          Trace("cegqi-qep") << "Result : " << qe_res << std::endl;
+      // create single invocation conjecture
+      Node qe_res_n = Node::fromExpr(qe_res);
+      qe_res_n = qe_res_n.substitute(
+          subs.begin(), subs.end(), orig.begin(), orig.end());
+      if (!nqe_vars.empty())
+      {
+        qe_res_n =
+            nm->mkNode(EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n);
+      }
+      Assert(q.getNumChildren() == 3);
+      qe_res_n = nm->mkNode(FORALL, q[0], qe_res_n, q[2]);
+      Trace("cegqi-qep") << "Converted conjecture after QE : " << qe_res_n
+                         << std::endl;
+      qe_res_n = Rewriter::rewrite(qe_res_n);
+      Node nq = qe_res_n;
+      // must assert it is equivalent to the original
+      Node lem = q.eqNode(nq);
+      Trace("cegqi-lemma") << "Cegqi::Lemma : qe-preprocess : " << lem
+                           << std::endl;
+      d_quantEngine->getOutputChannel().lemma(lem);
+      // we've reduced the original to a preprocessed version, return
+      return false;
+    }
+  }
+  d_conj->assign(q);
+  return true;
+}
 
-          // create single invocation conjecture
-          Node qe_res_n = Node::fromExpr(qe_res);
-          qe_res_n = qe_res_n.substitute(
-              subs.begin(), subs.end(), orig.begin(), orig.end());
-          if (!nqe_vars.empty())
-          {
-            qe_res_n = nm->mkNode(
-                EXISTS, nm->mkNode(BOUND_VAR_LIST, nqe_vars), qe_res_n);
-          }
-          Assert(conj.getNumChildren() == 3);
-          qe_res_n = nm->mkNode(FORALL, conj[0], qe_res_n, conj[2]);
-          Trace("cegqi-qep")
-              << "Converted conjecture after QE : " << qe_res_n << std::endl;
-          qe_res_n = Rewriter::rewrite(qe_res_n);
-          conj = qe_res_n;
-          // must assert it is equivalent to the original
-          Node lem = conj.eqNode(q);
-          Trace("cegqi-lemma")
-              << "Cegqi::Lemma : qe-preprocess : " << lem << std::endl;
-          d_quantEngine->getOutputChannel().lemma(lem);
-          // we've reduced the original to a preprocessed version, return
-          return;
-        }
+void CegInstantiation::registerQuantifier(Node q)
+{
+  if (d_quantEngine->getOwner(q) == this)
+  {  // && d_eval_axioms.find( q )==d_eval_axioms.end() ){
+    if (!d_conj->isAssigned())
+    {
+      Trace("cegqi") << "Register conjecture : " << q << std::endl;
+      if (options::sygusQePreproc())
+      {
+        d_waiting_conj = q;
+      }
+      else
+      {
+        // assign it now
+        d_conj->assign(q);
       }
-      d_conj->assign(conj);
     }else{
       Assert( d_conj->getEmbeddedConjecture()==q );
     }
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index 502244d25..03b4c4cc1 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -33,7 +33,20 @@ private:
   CegConjecture * d_conj;
   /** last instantiation by single invocation module? */
   bool d_last_inst_si;
-private:
+  /** the conjecture we are waiting to assign */
+  Node d_waiting_conj;
+
+ private:
+  /** assign quantified formula q as the conjecture
+   *
+   * This method returns true if q was successfully assigned as the synthesis
+   * conjecture considered by this class. This method may return false, for
+   * instance, if this class determines that it would rather rewrite q to
+   * an equivalent form r (in which case this method returns the lemma
+   * q <=> r). An example of this is the quantifier elimination step
+   * option::sygusQePreproc().
+   */
+  bool assignConjecture(Node q);
   /** check conjecture */
   void checkCegConjecture( CegConjecture * conj );
 public: