From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Jan 2022 21:46:38 +0000 (-0600)
Subject: Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)
X-Git-Tag: cvc5-1.0.0~557
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ffbdd1b3c3352fa342683facb44ca3e916844ac7;p=cvc5.git

Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)

This prevents the SyGuS subsolver from having a different configuration of dt-share-sel than the main SyGuS solver. Having this mismatch can lead to incorrect synthesis results.

Fixes #7925.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 23bf8ee6a..0335af870 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -677,6 +677,9 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   {
     if (logic.isQuantified() && !usesSygus(opts))
     {
+      Trace("smt")
+          << "Disabling shared selectors for quantified logic without SyGuS"
+          << std::endl;
       opts.datatypes.dtSharedSelectors = false;
     }
   }
diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 6b4796949..41b63cc53 100644
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
 #include "options/base_options.h"
+#include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -52,6 +53,11 @@ SynthVerify::SynthVerify(Env& env, TermDbSygus* tds)
   {
     d_subOptions.arith.nlExtTangentPlanes = true;
   }
+  // we must use the same setting for datatype selectors, since shared selectors
+  // can appear in solutions
+  d_subOptions.datatypes.dtSharedSelectors =
+      options().datatypes.dtSharedSelectors;
+  d_subOptions.datatypes.dtSharedSelectorsWasSetByUser = true;
 }
 
 SynthVerify::~SynthVerify() {}
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8cd30b38d..3bc432e5c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2537,6 +2537,7 @@ set(regress_1_tests
   regress1/sygus/issue4009-qep.smt2
   regress1/sygus/issue4025-no-rlv-cond.smt2
   regress1/sygus/issue4083-var-shadow.smt2
+  regress1/sygus/issue7925-dt-share-config.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
diff --git a/test/regress/regress1/sygus/issue7925-dt-share-config.sy b/test/regress/regress1/sygus/issue7925-dt-share-config.sy
new file mode 100644
index 000000000..f000e78a2
--- /dev/null
+++ b/test/regress/regress1/sygus/issue7925-dt-share-config.sy
@@ -0,0 +1,8 @@
+; COMMAND-LINE:
+; EXPECT: fail
+(set-logic ALL)
+(declare-datatypes ((wrapped_integer 0)) (((constructor (value Int)))))
+(synth-fun f ((input wrapped_integer)) Bool ((bool Bool)) ((bool Bool ( (= (value input) 0)))))
+(declare-var x wrapped_integer)
+(constraint (f x))
+(check-synth)