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 23bf8ee6aa1bd40a69c3126a7f8d82772a5a957f..0335af87057f541360da231a3a865234755b624b 100644 (file)
--- 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 6b47969495e683b4b9ea18ed90af17022773e3a8..41b63cc533adc25b28b27d8ffe96532107442d17 100644 (file)
--- 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 8cd30b38d064345f5cbc92632999f2402967870e..3bc432e5c982cf39fa83a8cec60750433ac2da4f 100644 (file)
--- 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 (file)
index 0000000..f000e78
--- /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)