Option to check solutions produced by SyGuS solver (#1553)

2 files changed, 118 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0c8723ff6..6af5e38d5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1353,13 +1353,13 @@ void SmtEngine::setDefaults() {
     */
   }
 
-  if(options::checkModels()) {
-    if(! options::produceAssertions()) {
+  if ((options::checkModels() || options::checkSynthSol())
+      && !options::produceAssertions())
+  {
       Notice() << "SmtEngine: turning on produce-assertions to support "
-               << "check-models." << endl;
+               << "check-models or check-synth-sol." << endl;
       setOption("produce-assertions", SExpr("true"));
     }
-  }
 
   if(options::unsatCores()) {
     if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
@@ -4801,6 +4801,12 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
         checkUnsatCore();
       }
     }
+    // Check that synthesis solutions satisfy the conjecture
+    if (options::checkSynthSol()
+        && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      checkSynthSolution();
+    }
 
     return r;
   } catch (UnsafeInterruptException& e) {
@@ -5488,6 +5494,104 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
+void SmtEngine::checkSynthSolution()
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
+  map<Node, Node> sol_map;
+  /* Get solutions and build auxiliary vectors for substituting */
+  d_theoryEngine->getSynthSolutions(sol_map);
+  Trace("check-synth-sol") << "Got solution map:\n";
+  std::vector<Node> function_vars, function_sols;
+  for (const auto& pair : sol_map)
+  {
+    Trace("check-synth-sol") << pair.first << " --> " << pair.second << "\n";
+    function_vars.push_back(pair.first);
+    function_sols.push_back(pair.second);
+  }
+  Trace("check-synth-sol") << "Starting new SMT Engine\n";
+  /* Start new SMT engine to check solutions */
+  SmtEngine solChecker(d_exprManager);
+  solChecker.setLogic(getLogicInfo());
+  setOption("check-synth-sol", SExpr("false"));
+
+  Trace("check-synth-sol") << "Retrieving assertions\n";
+  // Build conjecture from original assertions
+  if (d_assertionList == NULL)
+  {
+    Trace("check-synth-sol") << "No assertions to check\n";
+    return;
+  }
+  for (AssertionList::const_iterator i = d_assertionList->begin();
+       i != d_assertionList->end();
+       ++i)
+  {
+    Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << *i << endl;
+    Trace("check-synth-sol") << "Retrieving assertion " << *i << "\n";
+    Node conj = Node::fromExpr(*i);
+    // Apply any define-funs from the problem.
+    {
+      unordered_map<Node, Node, NodeHashFunction> cache;
+      conj = d_private->expandDefinitions(conj, cache);
+    }
+    Notice() << "SmtEngine::checkSynthSolution(): -- expands to " << conj << endl;
+    Trace("check-synth-sol") << "Expanded assertion " << conj << "\n";
+
+    // Apply solution map to conjecture body
+    Node conjBody;
+    /* Whether property is quantifier free */
+    if (conj[1].getKind() != kind::EXISTS)
+    {
+      conjBody = conj[1].substitute(function_vars.begin(),
+                                    function_vars.end(),
+                                    function_sols.begin(),
+                                    function_sols.end());
+    }
+    else
+    {
+      conjBody = conj[1][1].substitute(function_vars.begin(),
+                                       function_vars.end(),
+                                       function_sols.begin(),
+                                       function_sols.end());
+
+      /* Skolemize property */
+      std::vector<Node> vars, skos;
+      for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
+      {
+        vars.push_back(conj[1][0][j]);
+        std::stringstream ss;
+        ss << "sk_" << j;
+        skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
+        Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
+                                 << skos.back() << "\n";
+      }
+      conjBody = conjBody.substitute(
+          vars.begin(), vars.end(), skos.begin(), skos.end());
+    }
+    Notice() << "SmtEngine::checkSynthSolution(): -- body substitutes to "
+             << conjBody << endl;
+    Trace("check-synth-sol") << "Substituted body of assertion to " << conjBody
+                             << "\n";
+    solChecker.assertFormula(conjBody.toExpr());
+    Result r = solChecker.checkSat();
+    Notice() << "SmtEngine::checkSynthSolution(): result is " << r << endl;
+    Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
+    if (r.asSatisfiabilityResult().isUnknown())
+    {
+      InternalError(
+          "SmtEngine::checkSynthSolution(): could not check solution, result "
+          "unknown.");
+    }
+    else if (r.asSatisfiabilityResult().isSat())
+    {
+      InternalError(
+          "SmtEngine::checkSynhtSol(): produced solution allows satisfiable "
+          "negated conjecture.");
+    }
+    solChecker.resetAssertions();
+  }
+}
+
 // TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0501a6e8f..e768bf826 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -287,6 +287,16 @@ class CVC4_PUBLIC SmtEngine {
   void checkModel(bool hardFailure = true);
 
   /**
+   * Check that a solution to a synthesis conjecture is indeed a solution.
+   *
+   * The check is made by determining if the negation of the synthesis
+   * conjecture in which the functions-to-synthesize have been replaced by the
+   * synthesized solutions, which is a quantifier-free formula, is
+   * unsatisfiable. If not, then the found solutions are wrong.
+   */
+  void checkSynthSolution();
+
+  /**
    * Postprocess a value for output to the user.  Involves doing things
    * like turning datatypes back into tuples, length-1-bitvectors back
    * into booleans, etc.