Move sygus quantifier elimination step for non-ground-single-invocation to sygus (#2269)

2 files changed, 128 insertions, 121 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 15b6e2fc9..ab14904ff 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4826,125 +4826,7 @@ Result SmtEngine::checkSynth(const Expr& e)
   SmtScope smts(this);
   Trace("smt") << "Check synth: " << e << std::endl;
   Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
-  Expr e_check = e;
-  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 conj = Node::fromExpr(e);
-    if (conj.getKind() == kind::FORALL && conj[1].getKind() == kind::EXISTS)
-    {
-      Node conj_se = Node::fromExpr(expandDefinitions(conj[1][1].toExpr()));
-
-      Trace("smt-synth") << "Compute single invocation for " << conj_se << "..."
-                         << std::endl;
-      quantifiers::SingleInvocationPartition sip;
-      std::vector<Node> funcs;
-      funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
-      sip.init(funcs, conj_se.negate());
-      Trace("smt-synth") << "...finished, got:" << std::endl;
-      sip.debugPrint("smt-synth");
-
-      if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
-      {
-        // create new smt engine to do quantifier elimination
-        SmtEngine smt_qe(d_exprManager);
-        smt_qe.setLogic(getLogicInfo());
-        Trace("smt-synth") << "Property is non-ground single invocation, run "
-                              "QE to obtain single invocation."
-                           << std::endl;
-        NodeManager* nm = NodeManager::currentNM();
-        // 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; i < nqe_vars.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("smt-synth") << "  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("smt-synth") << "  subs : " << fi << " -> " << k << std::endl;
-        }
-        Node conj_se_ngsi = sip.getFullSpecification();
-        Trace("smt-synth") << "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(kind::EXISTS,
-                       nm->mkNode(kind::BOUND_VAR_LIST, qe_vars),
-                       conj_se_ngsi_subs.negate());
-
-        Trace("smt-synth") << "Run quantifier elimination on "
-                           << conj_se_ngsi_subs << std::endl;
-        Expr qe_res = smt_qe.doQuantifierElimination(
-            conj_se_ngsi_subs.toExpr(), true, false);
-        Trace("smt-synth") << "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(kind::EXISTS,
-                                nm->mkNode(kind::BOUND_VAR_LIST, nqe_vars),
-                                qe_res_n);
-        }
-        Assert(conj.getNumChildren() == 3);
-        qe_res_n = nm->mkNode(kind::FORALL, conj[0], qe_res_n, conj[2]);
-        Trace("smt-synth") << "Converted conjecture after QE : " << qe_res_n
-                           << std::endl;
-        e_check = qe_res_n.toExpr();
-      }
-    }
-  }
-
-  return checkSatisfiability( e_check, true, false );
+  return checkSatisfiability(e, true, false);
 }
 
 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index f877bcefd..919a8f008 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -16,11 +16,13 @@
 #include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 
 #include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/theory_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/theory_engine.h"
 
 using namespace CVC4::kind;
 using namespace std;
@@ -81,7 +83,130 @@ 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;
-      d_conj->assign( q );
+      Node conj = q;
+      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 " << conj << "..."
+                           << 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");
+
+        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;
+
+          // 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;
+        }
+      }
+      d_conj->assign(conj);
     }else{
       Assert( d_conj->getEmbeddedConjecture()==q );
     }