Tighten policy for unsat cores in sygus core connective (#7911)

Previous policy was due to limitations on options on subsolvers, which no longer exist.

Fixes cvc5/cvc5-projects#354.
Fixes #7902.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 67f4b8cda49eb2674f42b12017974ca7921e5dca..23bf8ee6aa1bd40a69c3126a7f8d82772a5a957f 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -352,17 +352,6 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const
 
 void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 {
-
-  // sygus core connective requires unsat cores
-  if (opts.quantifiers.sygusCoreConnective)
-  {
-    opts.smt.unsatCores = true;
-    if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
-    {
-      opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
-    }
-  }
-
   if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts
        || opts.smt.produceInterpols != options::ProduceInterpols::NONE
        || opts.smt.modelCoresMode != options::ModelCoresMode::NONE

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index e93d0a1055bd0df638090a22980e7ed9c6cfd9c0..bfc688db7397142a42c1f34f1ab19641ce4368a1 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -668,6 +668,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     // try a new core
     std::unique_ptr<SolverEngine> checkSol;
     initializeSubsolver(checkSol, d_env);
+    checkSol->setOption("produce-unsat-cores", "true");
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -709,6 +710,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("produce-unsat-cores", "true");
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5632cf438a6b4afa1a68c7151de0f9e945ef10e0..8b068aa3e83179da890d80e7abdb33c0a3c13dea 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1803,6 +1803,7 @@ set(regress_1_tests
   regress1/issue4335-unsat-core.smt2
   regress1/issue5101-alira-subtypes.smt2
   regress1/issue5739-rtf-processed.smt2
+  regress1/issue7902-abd-subsolver-uc.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/minimal_unsat_core.smt2

diff --git a/test/regress/regress1/issue7902-abd-subsolver-uc.smt2 b/test/regress/regress1/issue7902-abd-subsolver-uc.smt2
new file mode 100644 (file)
index 0000000..79a9dae
--- /dev/null
+++ b/test/regress/regress1/issue7902-abd-subsolver-uc.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; EXPECT: sat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-fun b () Bool)
+(assert (= b x))
+(check-sat)