Make sygus more robust to unknown responses in solution verification (#5199)

This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.

This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index da3a8dc8885711e29146c975648530f456f4b901..fad1b3dcdae0766699e13120a36a384476ff1454 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -460,7 +460,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-tplanes"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
 
 [[option]]

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 724a2ef2bb6b185a077690f160cc37c5c1da49b1..2a5faf9f746cbd68a7d1136bc6c515a4526aba56 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1310,14 +1310,6 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "enumerate a stream of solutions instead of terminating after the first one"
 
-[[option]]
-  name       = "sygusVerifySubcall"
-  category   = "regular"
-  long       = "sygus-verify-subcall"
-  type       = "bool"
-  default    = "true"
-  help       = "use separate copy of the SMT solver for verification lemmas in sygus"
-
 [[option]]
   name       = "sygusExtRew"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 468e246c4814228379c3fbd27a47fcd1644ac6b2..d9123e7f4f816a6ef467bd0b29b95fb858f5f579 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1117,6 +1117,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     {
       options::cegqiPreRegInst.set(true);
     }
+    // use tangent planes by default, since we want to put effort into
+    // the verification step for sygus queries with non-linear arithmetic
+    if (!options::nlExtTangentPlanes.wasSetByUser())
+    {
+      options::nlExtTangentPlanes.set(true);
+    }
     // not compatible with proofs
     if (options::proofNew())
     {

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0531d859d6d38ca21396827e8a153955310d6ccd..c65ac9e659cf6c8faae25c66cf933b71219668b3 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -617,26 +617,25 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     // either this conjecture does not have a solution, or candidate_values
     // is a solution for this conjecture.
     lem = nm->mkNode(OR, d_quant.negate(), query);
-    if (options::sygusVerifySubcall())
-    {
-      Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
+    Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
 
-      Result r =
-          checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
-      Trace("sygus-engine") << "  ...got " << r << std::endl;
-      if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+    Result r =
+        checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
+    Trace("sygus-engine") << "  ...got " << r << std::endl;
+    if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+    {
+      if (Trace.isOn("sygus-engine"))
       {
-        if (Trace.isOn("sygus-engine"))
+        Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
+        for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
         {
-          Trace("sygus-engine") << "  * Verification lemma failed for:\n   ";
-          for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
-          {
-            Trace("sygus-engine")
-                << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
-          }
-          Trace("sygus-engine") << std::endl;
+          Trace("sygus-engine")
+              << d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
         }
-#ifdef CVC4_ASSERTIONS
+        Trace("sygus-engine") << std::endl;
+      }
+      if (Configuration::isAssertionBuild())
+      {
         // the values for the query should be a complete model
         Node squery = query.substitute(d_ce_sk_vars.begin(),
                                        d_ce_sk_vars.end(),
@@ -647,20 +646,28 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
         Assert(options::sygusRecFun()
                || (squery.isConst() && squery.getConst<bool>()));
-#endif
-        return false;
       }
-      else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-      {
-        // if the result in the subcall was unsatisfiable, we avoid
-        // rechecking, hence we drop "query" from the verification lemma
-        lem = d_quant.negate();
-        // we can short circuit adding the lemma (for sygus stream)
-        success = true;
-      }
-      // In the rare case that the subcall is unknown, we add the verification
-      // lemma in the main solver. This should only happen if the quantifier
-      // free logic is undecidable.
+      return false;
+    }
+    else if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      // if the result in the subcall was unsatisfiable, we avoid
+      // rechecking, hence we drop "query" from the verification lemma
+      lem = d_quant.negate();
+      // we can short circuit adding the lemma (for sygus stream)
+      success = true;
+    }
+    else
+    {
+      // In the rare case that the subcall is unknown, we simply exclude the
+      // solution, without adding a counterexample point. This should only
+      // happen if the quantifier free logic is undecidable.
+      excludeCurrentSolution(terms, candidate_values);
+      // We should set incomplete, since a "sat" answer should not be
+      // interpreted as "infeasible", which would make a difference in the rare
+      // case where e.g. we had a finite grammar and exhausted the grammar.
+      d_qe->getOutputChannel().setIncomplete();
+      return false;
     }
   }
   if (success)