From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 25 Mar 2022 17:02:23 +0000 (-0500)
Subject: Fixes related to set defaults for sygus/proofs (#8395)
X-Git-Tag: cvc5-1.0.0~176
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3ba5a8eca70539ac00719eb3de68cb214033c59;p=cvc5.git

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 5e987b862..9f322f487 100644
--- 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 ae23d3ae6..d24bf916c 100644
--- 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 f3e135cdc..7e58a1e14 100644
--- 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());