From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Mar 2020 17:41:49 +0000 (-0500)
Subject: Handle failures for sygus QE preprocess (#4072)
X-Git-Tag: cvc5-1.0.0~3467
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed2aa5d552a86fe3e4798ef03c995f54abe20cb9;p=cvc5.git

Handle failures for sygus QE preprocess (#4072)

If the user explicitly disabled the QE algorithm and asked for QE, then we should resort to normal methods. Fixes #4064 and fixes #4109.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d3ba34b6c..a367c8469 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5164,9 +5164,11 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   Trace("smt-qe") << "Query returned " << r << std::endl;
   if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
     if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
-      InternalError()
+      Notice()
           << "While performing quantifier elimination, unexpected result : "
           << r << " for query.";
+      // failed, return original
+      return e;
     }
     std::vector< Node > inst_qs;
     d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 978e31545..0c8b8f734 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -15,6 +15,7 @@
  **/
 #include "theory/quantifiers/sygus/synth_engine.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -236,28 +237,31 @@ void SynthEngine::assignConjecture(Node q)
           conj_se_ngsi_subs.toExpr(), true, false);
       Trace("cegqi-qep") << "Result : " << qe_res << std::endl;
 
-      // create single invocation conjecture
+      // create single invocation conjecture, if QE was successful
       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())
+      if (!expr::hasBoundVar(qe_res_n))
       {
-        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
+        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;
-      d_quantEngine->getOutputChannel().lemma(lem);
-      // we've reduced the original to a preprocessed version, return
-      return;
+        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;
+      }
     }
   }
   // allocate a new synthesis conjecture if not assigned