Generalization for sygus verify utility (#8586)

This is in preparation for synthesis modulo oracles (SyMO), where the verification loop may run multiple times for a given solution. In a follow up PR, the loop introduced in this PR may run multiple times when oracles are present, since oracle invocations in the subsolver may trigger further simplifications to the rewritten form of the specification.

It also makes it so that candidate models are generated for "unknown" results for subsolvers, which is required for SyMO.

diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 82e356c48ba4803cbafe25b2664f0639e18ffcb5..e5bab459db8b8811013e34c5e9b5a5610139cf6f 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -65,22 +65,74 @@ SynthVerify::~SynthVerify() {}
 Result SynthVerify::verify(Node query,
                            const std::vector<Node>& vars,
                            std::vector<Node>& mvs)
+{
+  Node queryp = preprocessQueryInternal(query);
+  bool finished;
+  Result r;
+  do
+  {
+    Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
+    if (queryp.isConst())
+    {
+      if (!queryp.getConst<bool>())
+      {
+        return Result(Result::UNSAT);
+      }
+      // sat, but we need to get arbtirary model values below
+    }
+    r = checkWithSubsolver(queryp,
+                           vars,
+                           mvs,
+                           d_subOptions,
+                           d_subLogicInfo,
+                           options().quantifiers.sygusVerifyTimeout != 0,
+                           options().quantifiers.sygusVerifyTimeout);
+    finished = true;
+    Trace("sygus-engine") << "  ...got " << r << std::endl;
+    // we try to learn models for "sat" and "unknown" here
+    if (r.getStatus() != Result::UNSAT)
+    {
+      if (TraceIsOn("sygus-engine"))
+      {
+        Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
+        for (unsigned i = 0, size = vars.size(); i < size; i++)
+        {
+          Trace("sygus-engine") << vars[i] << " -> " << mvs[i] << " ";
+        }
+        Trace("sygus-engine") << std::endl;
+      }
+      // check whether the query is satisfied by the model
+      if (Configuration::isAssertionBuild())
+      {
+        Assert(vars.size() == mvs.size());
+        // the values for the query should be a complete model
+        Node squery =
+            query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end());
+        Trace("cegqi-debug") << "...squery : " << squery << std::endl;
+        squery = d_tds->rewriteNode(squery);
+        Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
+        // if the query simplifies to false, then something
+        // went wrong or the answer is unknown (for debugging).
+        if (squery.isConst() && !squery.getConst<bool>())
+        {
+          Assert(r.getStatus() == Result::UNKNOWN)
+              << "Expected model from verification step to satisfy query";
+        }
+      }
+    }
+  } while (!finished);
+  return r;
+}
+
+Node SynthVerify::preprocessQueryInternal(Node query)
 {
   NodeManager* nm = NodeManager::currentNM();
+  Trace("cegqi-debug") << "pre-rewritten query : " << query << std::endl;
   // simplify the lemma based on the term database sygus utility
   query = d_tds->rewriteNode(query);
   // eagerly unfold applications of evaluation function
-  Trace("cegqi-debug") << "pre-unfold counterexample : " << query << std::endl;
-
-  if (query.isConst())
-  {
-    if (!query.getConst<bool>())
-    {
-      return Result(Result::UNSAT);
-    }
-    // sat, but we need to get arbtirary model values below
-  }
-  else
+  Trace("cegqi-debug") << "post-rewritten query : " << query << std::endl;
+  if (!query.isConst())
   {
     // if non-constant, we may need to add recursive function definitions
     FunDefEvaluator* feval = d_tds->getFunDefEvaluator();
@@ -98,6 +150,7 @@ Result SynthVerify::verify(Node query,
       qconj.push_back(query);
       for (const Node& f : syms)
       {
+        // get the function definition
         Node q = feval->getDefinitionFor(f);
         if (!q.isNull())
         {
@@ -105,43 +158,11 @@ Result SynthVerify::verify(Node query,
         }
       }
       query = nm->mkAnd(qconj);
-      Trace("cegqi-debug") << "query is " << query << std::endl;
-    }
-  }
-  Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
-  query = rewrite(query);
-  Result r = checkWithSubsolver(query,
-                                vars,
-                                mvs,
-                                d_subOptions,
-                                d_subLogicInfo,
-                                options().quantifiers.sygusVerifyTimeout != 0,
-                                options().quantifiers.sygusVerifyTimeout);
-  Trace("sygus-engine") << "  ...got " << r << std::endl;
-  if (r.getStatus() == Result::SAT)
-  {
-    if (TraceIsOn("sygus-engine"))
-    {
-      Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
-      for (unsigned i = 0, size = vars.size(); i < size; i++)
-      {
-        Trace("sygus-engine") << vars[i] << " -> " << mvs[i] << " ";
-      }
-      Trace("sygus-engine") << std::endl;
-    }
-    if (Configuration::isAssertionBuild())
-    {
-      // the values for the query should be a complete model
-      Node squery =
-          query.substitute(vars.begin(), vars.end(), mvs.begin(), mvs.end());
-      Trace("cegqi-debug") << "...squery : " << squery << std::endl;
-      squery = rewrite(squery);
-      Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
-      Assert(options().quantifiers.sygusRecFun
-             || (squery.isConst() && squery.getConst<bool>()));
+      Trace("cegqi-debug") << "after function definitions, query is " << query
+                           << std::endl;
     }
   }
-  return r;
+  return query;
 }
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h
index 2a4e50b196b65458f78f388e7a22c1b96de13de5..37d02103251b3add3f0e219a3b1a0ae6c43e548d 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.h
+++ b/src/theory/quantifiers/sygus/synth_verify.h
@@ -52,6 +52,12 @@ class SynthVerify : protected EnvObj
                 std::vector<Node>& mvs);
 
  private:
+  /**
+   * Preprocess query internal. This returns the rewritten form of query
+   * and includes all relevant function definitions, i.e. those that occur
+   * in query. These are added as top-level conjuncts to the returned formula.
+   */
+  Node preprocessQueryInternal(Node query);
   /** Pointer to the term database sygus */
   TermDbSygus* d_tds;
   /** The options for subsolver calls */

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 2cda7d2c3dacb8af30e11a2d6b5531f237d11c19..bb9f4cb2fb1f5b0f2c15bf4be418ca39a098145a 100644 (file)
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -126,7 +126,7 @@ Result checkWithSubsolver(Node query,
   initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
   smte->assertFormula(query);
   r = smte->checkSat();
-  if (r.getStatus() == Result::SAT)
+  if (r.getStatus() == Result::SAT || r.getStatus() == Result::UNKNOWN)
   {
     for (const Node& v : vars)
     {