From ffbdd1b3c3352fa342683facb44ca3e916844ac7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Jan 2022 15:46:38 -0600 Subject: [PATCH] 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. --- src/smt/set_defaults.cpp | 3 +++ src/theory/quantifiers/sygus/synth_verify.cpp | 6 ++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress1/sygus/issue7925-dt-share-config.sy | 8 ++++++++ 4 files changed, 18 insertions(+) create mode 100644 test/regress/regress1/sygus/issue7925-dt-share-config.sy 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) -- 2.30.2