Make sygus infer find function definitions (#1951)

4 files changed, 85 insertions, 13 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index fc7ec8e52..03c39f718 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -105,7 +105,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
         rrChecker.assertFormula(crr.toExpr());
         Result r = rrChecker.checkSat();
         Trace("rr-check") << "...result : " << r << std::endl;
-        if (r.asSatisfiabilityResult().isSat())
+        if (r.asSatisfiabilityResult().isSat() == Result::SAT)
         {
           Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
           success = false;
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 1ca1902a1..f9208599f 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -209,7 +209,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
   repcChecker.assertFormula(fo_body.toExpr());
   Result r = repcChecker.checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
-  if (r.asSatisfiabilityResult().isSat()
+  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT
       && !r.asSatisfiabilityResult().isUnknown())
   {
     std::vector<Node> sk_sygus_m;
diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp
index cea992f54..dc6ca56a4 100644
--- a/src/theory/quantifiers/sygus_inference.cpp
+++ b/src/theory/quantifiers/sygus_inference.cpp
@@ -13,6 +13,9 @@
  **/
 
 #include "theory/quantifiers/sygus_inference.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
@@ -85,6 +88,15 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
     }
     if (pas.getKind() == FORALL)
     {
+      // it must be a standard quantifier
+      QAttributes qa;
+      QuantAttributes::computeQuantAttributes(pas, qa);
+      if (!qa.isStandard())
+      {
+        Trace("sygus-infer")
+            << "...fail: non-standard top-level quantifier." << std::endl;
+        return false;
+      }
       // infer prefix
       for (const Node& v : pas[0])
       {
@@ -170,10 +182,13 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
   // for each free function symbol, make a bound variable of the same type
   Trace("sygus-infer") << "Do free function substitution..." << std::endl;
   std::vector<Node> ff_vars;
+  std::map<Node, Node> ff_var_to_ff;
   for (const Node& ff : free_functions)
   {
     Node ffv = nm->mkBoundVar(ff.getType());
     ff_vars.push_back(ffv);
+    Trace("sygus-infer") << "  synth-fun: " << ff << " as " << ffv << std::endl;
+    ff_var_to_ff[ffv] = ff;
   }
   // substitute free functions -> variables
   body = body.substitute(free_functions.begin(),
@@ -204,17 +219,66 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
 
   Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
 
-  // replace all assertions except the first with true
-  Node truen = nm->mkConst(true);
-  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+  // make a separate smt call
+  SmtEngine* master_smte = smt::currentSmtEngine();
+  SmtEngine rrSygus(nm->toExprManager());
+  rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo());
+  rrSygus.assertFormula(body.toExpr());
+  Trace("sygus-infer") << "*** Check sat..." << std::endl;
+  Result r = rrSygus.checkSat();
+  Trace("sygus-infer") << "...result : " << r << std::endl;
+  if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+  {
+    // failed, conjecture was infeasible
+    return false;
+  }
+  // get the synthesis solutions
+  std::map<Expr, Expr> synth_sols;
+  rrSygus.getSynthSolutions(synth_sols);
+
+  std::vector<Node> final_ff;
+  std::vector<Node> final_ff_sol;
+  for (std::map<Expr, Expr>::iterator it = synth_sols.begin();
+       it != synth_sols.end();
+       ++it)
   {
-    if (i == 0)
+    Node lambda = Node::fromExpr(it->second);
+    Trace("sygus-infer") << "  synth sol : " << it->first << " -> "
+                         << it->second << std::endl;
+    Node ffv = Node::fromExpr(it->first);
+    std::map<Node, Node>::iterator itffv = ff_var_to_ff.find(ffv);
+    // all synthesis solutions should correspond to a variable we introduced
+    Assert(itffv != ff_var_to_ff.end());
+    if (itffv != ff_var_to_ff.end())
     {
-      assertions[i] = body;
+      Node ff = itffv->second;
+      std::vector<Expr> args;
+      for (const Node& v : lambda[0])
+      {
+        args.push_back(v.toExpr());
+      }
+      Trace("sygus-infer") << "Define " << ff << " as " << it->second
+                           << std::endl;
+      final_ff.push_back(ff);
+      final_ff_sol.push_back(it->second);
+      master_smte->defineFunction(ff.toExpr(), args, it->second[1]);
     }
-    else
+  }
+
+  // apply substitution to everything, should result in SAT
+  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+  {
+    Node prev = assertions[i];
+    Node curr = assertions[i].substitute(final_ff.begin(),
+                                         final_ff.end(),
+                                         final_ff_sol.begin(),
+                                         final_ff_sol.end());
+    if (curr != prev)
     {
-      assertions[i] = truen;
+      curr = Rewriter::rewrite(curr);
+      Trace("sygus-infer-debug")
+          << "...rewrote " << prev << " to " << curr << std::endl;
+      assertions[i] = curr;
     }
   }
   return true;
diff --git a/src/theory/quantifiers/sygus_inference.h b/src/theory/quantifiers/sygus_inference.h
index a61cebcc0..cdd5a1008 100644
--- a/src/theory/quantifiers/sygus_inference.h
+++ b/src/theory/quantifiers/sygus_inference.h
@@ -26,8 +26,12 @@ namespace quantifiers {
 
 /** SygusInference
  *
- * A preprocessing utility to turn a set of (quantified) assertions into a
- * single SyGuS conjecture.
+ * A preprocessing utility that turns a set of (quantified) assertions into a
+ * single SyGuS conjecture. If this is possible, we solve for this single Sygus
+ * conjecture using a separate copy of the SMT engine. If sygus successfully
+ * solves the conjecture, we plug the synthesis solutions back into the original
+ * problem, thus obtaining a set of model substitutions under which the
+ * assertions should simplify to true.
  */
 class SygusInference
 {
@@ -36,8 +40,12 @@ class SygusInference
   ~SygusInference() {}
   /** simplify assertions
    *
-   * Either replaces assertions with the negation of an equivalent SyGuS
-   * conjecture and returns true, or otherwise returns false.
+   * Either replaces all uninterpreted functions in assertions by their
+   * interpretation in the solution found by a separate call to an SMT engine
+   * and returns true, or leaves the assertions unmodified and returns false.
+   *
+   * We fail if either a sygus conjecture that corresponds to assertions cannot
+   * be inferred, or the sygus conjecture we infer is infeasible.
    */
   bool simplify(std::vector<Node>& assertions);
 };