Make sygus infer find function definitions (#1951)

8 files changed, 140 insertions, 25 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 82147c094..36792e3c0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2701,7 +2701,9 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, Node
       // otherwise expand it
       bool doExpand = k == kind::APPLY;
       if( !doExpand ){
-        if( options::macrosQuant() ){
+        // options that assign substitutions to APPLY_UF
+        if (options::macrosQuant() || options::sygusInference())
+        {
           //expand if we have inferred an operator corresponds to a defined function
           doExpand = k==kind::APPLY_UF && d_smt.isDefinedFunction( n.getOperator().toExpr() );
         }
@@ -4004,17 +4006,7 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  if (options::sygusInference())
-  {
-    // try recast as sygus
-    quantifiers::SygusInference si;
-    if (si.simplify(d_assertions.ref()))
-    {
-      Trace("smt-proc") << "...converted to sygus conjecture." << std::endl;
-      d_smt.d_globalNegation = !d_smt.d_globalNegation;
-    }
-  }
-  else if (options::globalNegate())
+  if (options::globalNegate())
   {
     // global negation of the formula
     quantifiers::GlobalNegate gn;
@@ -4211,6 +4203,15 @@ void SmtEnginePrivate::processAssertions() {
         d_smt.d_fmfRecFunctionsDefined->push_back( f );
       }
     }
+    if (options::sygusInference())
+    {
+      // try recast as sygus
+      quantifiers::SygusInference si;
+      if (si.simplify(d_assertions.ref()))
+      {
+        Trace("smt-proc") << "...converted to sygus conjecture." << std::endl;
+      }
+    }
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl;
   }
 
@@ -5573,6 +5574,18 @@ void SmtEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
+void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
+{
+  SmtScope smts(this);
+  map<Node, Node> sol_mapn;
+  Assert(d_theoryEngine != nullptr);
+  d_theoryEngine->getSynthSolutions(sol_mapn);
+  for (std::pair<const Node, Node>& s : sol_mapn)
+  {
+    sol_map[s.first.toExpr()] = s.second.toExpr();
+  }
+}
+
 Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
 {
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 83300afc9..dd1d1b88a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -656,6 +656,22 @@ class CVC4_PUBLIC SmtEngine {
   void printSynthSolution( std::ostream& out );
 
   /**
+   * Get synth solution
+   *
+   * This function adds entries to sol_map that map functions-to-synthesize with
+   * their solutions, for all active conjectures. This should be called
+   * immediately after the solver answers unsat for sygus input.
+   *
+   * Specifically, given a sygus conjecture of the form
+   *   exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
+   * where x1...xn are second order bound variables, we map each xi to
+   * lambda term in sol_map such that
+   *    forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
+   * is a valid formula.
+   */
+  void getSynthSolutions(std::map<Expr, Expr>& sol_map);
+
+  /**
    * Do quantifier elimination.
    *
    * This function takes as input a quantified formula e
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);
 };
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 72bf64ac8..ed2390fe5 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1249,6 +1249,7 @@ REG1_TESTS = \
 	regress1/quantifiers/extract-nproc.smt2 \
 	regress1/quantifiers/florian-case-ax.smt2 \
 	regress1/quantifiers/gauss_init_0030.fof.smt2 \
+	regress1/quantifiers/horn-simple.smt2 \
 	regress1/quantifiers/inst-max-level-segf.smt2 \
 	regress1/quantifiers/inst-prop-simp.smt2 \
 	regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \
diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2
new file mode 100644
index 000000000..a27d8e0d6
--- /dev/null
+++ b/test/regress/regress1/quantifiers/horn-simple.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --sygus-unif --sygus-infer
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun I (Int) Bool)
+
+(assert (forall ((x Int)) (=> (= x 0) (I x))))
+
+(assert (forall ((x Int)) (=> (and (I x) (< x 1)) (I (+ x 1)))))
+
+(assert (forall ((x Int)) (=> (I x) (<= x 10))))
+
+(check-sat)