Fixes related to set defaults for sygus/proofs (#8395)

This ensures we always report that SyGuS is incompatible with proofs. As a result, we require disabling sygus in 2 contexts where it should have been disabled before.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 5e987b862163165b474d12c7d4c1b0d3ffa8c998..9f322f4877bf30961306bf55b7f8c37fcfe19f4d 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -913,6 +913,15 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
     reason << "global-negate";
     return true;
   }
+  if (isSygus(opts))
+  {
+    // we don't support proofs with SyGuS. One issue is that SyGuS evaluation
+    // functions are incompatible with our equality proofs. Moreover, enabling
+    // proofs for sygus (sub)solvers is irrelevant, since they are not given
+    // check-sat queries.
+    reason << "sygus";
+    return true;
+  }
   // options that are automatically set to support proofs
   if (opts.bv.bvAssertInput)
   {

diff --git a/src/theory/quantifiers/query_generator_unsat.cpp b/src/theory/quantifiers/query_generator_unsat.cpp
index ae23d3ae636bdb4e56a61088f9d7d8c71bd26ef9..d24bf916cd20953a34e773bbdf4164ee9669fca8 100644 (file)
--- a/src/theory/quantifiers/query_generator_unsat.cpp
+++ b/src/theory/quantifiers/query_generator_unsat.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/quantifiers/query_generator_unsat.h"
 
+#include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
 #include "util/random.h"
@@ -31,6 +32,7 @@ QueryGeneratorUnsat::QueryGeneratorUnsat(Env& env) : QueryGenerator(env)
   // determine the options to use for the verification subsolvers we spawn
   // we start with the provided options
   d_subOptions.copyValues(d_env.getOriginalOptions());
+  d_subOptions.quantifiers.sygus = false;
   d_subOptions.smt.produceProofs = true;
   d_subOptions.smt.checkProofs = true;
   d_subOptions.smt.produceModels = true;

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index f3e135cdc46ea20df7616ced9306ec34ae5fc047..7e58a1e14f9a4fa528615b61c4bb63494b2d9a9a 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -712,6 +712,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
           std::unique_ptr<SolverEngine> checkSc;
           initializeSubsolver(checkSc, d_env);
+          checkSc->setOption("sygus", "false");
           checkSc->setOption("produce-unsat-cores", "true");
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());