Implement internal support for synthesis modulo oracles (#8617)

SyMO is implemented as a preprocessor for SMT queries in the verification subsolver of SyGuS.

diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index e5bab459db8b8811013e34c5e9b5a5610139cf6f..3f78a8d42b4ed637f9a7fae3fc76d3dbb522566f 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -102,21 +102,43 @@ Result SynthVerify::verify(Node query,
         Trace("sygus-engine") << std::endl;
       }
       // check whether the query is satisfied by the model
-      if (Configuration::isAssertionBuild())
+      if (options().quantifiers.oracles || 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;
+        // Rewrite the node. Notice that if squery contains oracle function
+        // symbols, then this may trigger new calls to oracles.
         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>())
+        if (!squery.isConst() || !squery.getConst<bool>())
         {
-          Assert(r.getStatus() == Result::UNKNOWN)
-              << "Expected model from verification step to satisfy query";
+          // If the query did not simplify to true, then it may be that the
+          // value for an oracle function was not what we expected.
+          if (options().quantifiers.oracles)
+          {
+            // In this case, we reconstruct the query, which may include more
+            // information about oracles than we had previously, due to the
+            // call to rewriteNode above. We rerun the satisfiability check
+            // above, which now may conjoin more I/O pairs to the preprocessed
+            // query.
+            Node nextQueryp = preprocessQueryInternal(query);
+            if (nextQueryp != queryp)
+            {
+              queryp = nextQueryp;
+              finished = false;
+            }
+          }
+          else if (squery.isConst())
+          {
+            // simplified to false, the result should have been unknown, or
+            // else this indicates a check-model failure. We check this only
+            // if oracles are disabled.
+            Assert(r.getStatus() == Result::UNKNOWN)
+                << "Expected model from verification step to satisfy query";
+          }
         }
       }
     }
@@ -136,8 +158,9 @@ Node SynthVerify::preprocessQueryInternal(Node query)
   {
     // if non-constant, we may need to add recursive function definitions
     FunDefEvaluator* feval = d_tds->getFunDefEvaluator();
+    OracleChecker* ochecker = d_tds->getOracleChecker();
     const std::vector<Node>& fdefs = feval->getDefinitions();
-    if (!fdefs.empty())
+    if (!fdefs.empty() || (ochecker != nullptr && ochecker->hasOracles()))
     {
       // Get the relevant definitions based on the symbols in the query.
       // Notice in some cases, this may have the effect of making the subcall
@@ -156,10 +179,24 @@ Node SynthVerify::preprocessQueryInternal(Node query)
         {
           qconj.push_back(q);
         }
+        // Get the relevant cached oracle calls.
+        // In contrast to the presentation in Polgreen et al VMCAI 2022,
+        // we do not use SMTO as a subsolver for SyMO here. Instead, we
+        // conjoin the set of I/O pairs known about each oracle function
+        // to the query.
+        if (ochecker != nullptr && ochecker->hasOracleCalls(f))
+        {
+          const std::map<Node, Node>& ocalls = ochecker->getOracleCalls(f);
+          for (const std::pair<const Node, Node>& oc : ocalls)
+          {
+            qconj.push_back(oc.first.eqNode(oc.second));
+          }
+        }
       }
       query = nm->mkAnd(qconj);
-      Trace("cegqi-debug") << "after function definitions, query is " << query
-                           << std::endl;
+      Trace("cegqi-debug")
+          << "after function definitions + oracle calls, query is " << query
+          << std::endl;
     }
   }
   return query;

diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h
index 37d02103251b3add3f0e219a3b1a0ae6c43e548d..1f301ef1a6a9793b6ad35387368fafbf1d85a9df 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_verify.h
+++ b/src/theory/quantifiers/sygus/synth_verify.h
@@ -56,6 +56,12 @@ class SynthVerify : protected EnvObj
    * 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.
+   *
+   * For each oracle function f in the query, we conjoin equalities f(c) = d
+   * where (c, d) is an I/O pair obtained for a call to a oracle. In contrast
+   * to the description in Polgreen et al VMCAI 2022, the verification subcall
+   * uses SMT, not SMTO. Instead f is treated as an ordinary function symbol,
+   * and its current I/O pairs are communicated explicitly via these conjuncts.
    */
   Node preprocessQueryInternal(Node query);
   /** Pointer to the term database sygus */