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

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 9d717c0ba4bf77765cfbf846d513bbd62e15e224..96d73feebd03003da5727a91730726f5741315c3 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -294,10 +294,10 @@ option sygusCRefEval --sygus-cref-eval bool :default true
   direct evaluation of refinement lemmas for conflict analysis
 option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true
   use min explain for direct evaluation of refinement lemmas for conflict analysis
-  
+
 option sygusStream --sygus-stream bool :read-write :default false
   enumerate a stream of solutions instead of terminating after the first one
-  
+
 # internal uses of sygus
 option sygusRewSynth --sygus-rr-synth bool :default false
   use sygus to enumerate candidate rewrite rules via sampling

diff --git a/src/options/smt_options b/src/options/smt_options
index fa6c3ae4e9be50f6a153509d49494b700ed0df51..b19420060f76d0361aa7ab00f803c058a021f6f7 100644 (file)
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -54,6 +54,9 @@ option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-uns
 option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch
  dump the full unsat core, including unlabeled assertions
 
+option checkSynthSol --check-synth-sol bool :default false
+ checks whether produced solutions to functions-to-synthesize satisfy the conjecture
+
 option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch
  support the get-assignment command
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0c8723ff67365afa0f106a9ce4747343df82e0be..6af5e38d58c58c5c59cc3d52fabfee832f700b5e 100644 (file)
--- 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 0501a6e8fd72bc51fb12179eafa22f411ea12d7c..e768bf826bcda0b25c95b1749dac51f22b852ea0 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -286,6 +286,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

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 34dde7fc8dc09e41cae2abcfcd0cec918e6bc16a..a0efe80f9aeb1954c2e53c9bf080394ce142eedc 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1195,6 +1195,11 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
   return ret;
 }
 
+void QuantifiersEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+{
+  d_ceg_inst->getSynthSolutions(sol_map);
+}
+
 void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
   eq::EqualityEngine* ee = getActiveEqualityEngine();
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 3cd4e8ef9e4f10d40df3deea90f8782f58abb729..3716fc49770fdb49136def91fd9a1c46b9434b59 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -399,6 +399,18 @@ public:
   void getExplanationForInstLemmas(const std::vector<Node>& lems,
                                    std::map<Node, Node>& quant,
                                    std::map<Node, std::vector<Node> >& tvec);
+
+  /** get synth solutions
+   *
+   * 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.
+   *
+   * For details on what is added to sol_map, see
+   * CegConjecture::getSynthSolutions.
+   */
+  void getSynthSolutions(std::map<Node, Node>& sol_map);
+
   //----------end user interface for instantiations
 
   /** statistics class */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 435dadce7f2acb6af86b768e54c9b435d829b2f8..edbd768d7375c3e181caa5a81c73eae6165e44c2 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -902,6 +902,11 @@ TheoryModel* TheoryEngine::getModel() {
   return d_curr_model;
 }
 
+void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+{
+  d_quantEngine->getSynthSolutions(sol_map);
+}
+
 bool TheoryEngine::presolve() {
   // Reset the interrupt flag
   d_interrupted = false;

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 22e2694095ad24678031c85de99feacb6f93122f..7bc95b097b1b57e15455b92016563e5e7700430d 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -715,6 +715,17 @@ public:
    */
   theory::TheoryModel* getModel();
 
+  /** get synth solutions
+   *
+   * 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.
+   *
+   * For details on what is added to sol_map, see
+   * CegConjecture::getSynthSolutions.
+   */
+  void getSynthSolutions(std::map<Node, Node>& sol_map);
+
   /**
    * Get the model builder
    */

diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index 1792749e275e781cfa2a855efa0e745bde80b61b..33552f9e2cfbe83cfbf5d6243117daace894de30 100755 (executable)
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol
 (set-logic LIA)
 
 (synth-fun fb () Int ((Start Int ((Constant Int)))))

diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index 41346e65530a891a74db580c2fcbb238848ee10f..5786eb649dc3651b333702cc86d2f0f4f921311b 100644 (file)
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)

diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index 305f5783a5a0f499436fdcb5a58452cec9527f50..af2d8b25bec41ca97fb2eaf916ab248612b55a11 100644 (file)
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol
 
 (set-logic LIA)
 

diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index 37ed848efbf93ddb886622840b8daa5b4a06ac01..cbe2bccea68af8eb9df9a08a2651c3038eff3d88 100644 (file)
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int

diff --git a/test/regress/run_regression b/test/regress/run_regression
index 5d41655973290fe6515a6db97caa9ad6d3269e49..e236234e111a6df31cb2d4dbb96720d3741d7fda 100755 (executable)
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -262,6 +262,13 @@ else
   echo "$expected_output" >"$expoutfile"
 fi
 
+if [ "$lang" = sygus ]; then
+  if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-synth-sol' &>/dev/null &&
+     ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-synth-sol' &>/dev/null; then
+    # later on, we'll run another test with --check-models on
+    command_line="$command_line --check-synth-sol"
+  fi
+fi
 check_models=false
 if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then
   if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null &&
@@ -407,4 +414,5 @@ if $check_models || $check_proofs || $check_unsat_cores; then
   fi
 fi
 
+
 exit $exitcode