Disable shared selectors for quantified logics without SyGuS (#7156)

The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.

This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c35c2961..1e21abc47 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -702,6 +702,16 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
   // set all defaults in the quantifiers theory, which includes sygus
   setDefaultsQuantifiers(logic, opts);
 
+  // shared selectors are generally not good to combine with standard
+  // quantifier techniques e.g. E-matching
+  if (opts.datatypes.dtSharedSelectorsWasSetByUser)
+  {
+    if (logic.isQuantified() && !usesSygus(opts))
+    {
+      opts.datatypes.dtSharedSelectors = false;
+    }
+  }
+
   // until bugs 371,431 are fixed
   if (!opts.prop.minisatUseElimWasSetByUser)
   {