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.

6 files changed, 97 insertions, 2 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)
   {
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index e41bef015..33d143a36 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -199,8 +199,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
           for (size_t i = 0, vsize = c[0].getNumChildren(); i < vsize; i++)
           {
             vars.push_back(c[0][i]);
-            Node sc = nm->mkNode(
-                APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(t, i), h);
+            Node sc =
+                nm->mkNode(APPLY_SELECTOR, dt[cindex][i].getSelector(), h);
             subs.push_back(sc);
           }
         }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7ba3c9758..eb8102856 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -24,6 +24,16 @@ namespace cvc5 {
 namespace theory {
 namespace datatypes {
 
+/**
+ * The rewriter for datatypes. An invariant of the rewriter is that
+ * postRewrite/preRewrite should not depend on the options, in particular,
+ * they should not depend on whether shared selectors are enabled. Thus,
+ * they should not use DTypeConstructor::getSelectorInternal. Instead,
+ * the conversion from external to internal selectors is done in
+ * expandDefinition. This invariant ensures that the rewritten form of a node
+ * does not mix multiple option settings, which would lead to e.g. shared
+ * selectors being used in an SmtEngine instance where they are disabled.
+ */
 class DatatypesRewriter : public TheoryRewriter
 {
  public:
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 80f4af984..9c43e8b51 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -228,6 +228,9 @@ bool CegSingleInv::solve()
   // solve the single invocation conjecture using a fresh copy of SMT engine
   std::unique_ptr<SmtEngine> siSmt;
   initializeSubsolver(siSmt, d_env);
+  // do not use shared selectors in subsolver, since this leads to solutions
+  // with non-user symbols
+  siSmt->setOption("dt-share-sel", "false");
   siSmt->assertFormula(siq);
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8909bfc06..852734772 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2331,6 +2331,7 @@ set(regress_1_tests
   regress1/sygus/interpol_from_pono_2.smt2
   regress1/sygus/issue2914.sy
   regress1/sygus/issue2935.sy
+  regress1/sygus/issue3109-share-sel.sy
   regress1/sygus/issue3199.smt2
   regress1/sygus/issue3200.smt2
   regress1/sygus/issue3201.smt2
diff --git a/test/regress/regress1/sygus/issue3109-share-sel.sy b/test/regress/regress1/sygus/issue3109-share-sel.sy
new file mode 100644
index 000000000..4b08a937d
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3109-share-sel.sy
@@ -0,0 +1,71 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(declare-datatypes ((IntRange 0)) 
+   (((IntRange (lower Int) (upper Int)))))
+
+(declare-datatypes ((Loc 0)) 
+   (((Loc (x Int) (y Int)))))
+
+(declare-datatypes ((LocRange 0)) 
+   (((LocRange (xD IntRange) (yD IntRange)))))
+
+(declare-datatypes ((Ship 0)) 
+   (((Ship (shipCapacity Int) (shipLoc Loc)))))
+
+(declare-datatypes ((ShipRange 0)) 
+   (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange)))))
+
+(define-fun betweenInt ((x Int) (r IntRange)) Bool
+    (and (< (lower r) x) (< x (upper r)))
+)
+
+(define-fun betweenLoc ((l Loc) (lr LocRange)) Bool
+    (and (betweenInt (x l) (xD lr)) (betweenInt (y l) (yD lr)))
+)
+
+(define-fun subsetInt ((r1 IntRange) (r2 IntRange)) Bool
+    (and (>= (lower r1) (lower r2)) (<= (upper r1) (upper r2)))
+)
+
+(define-fun betweenShip ((s Ship) (sr ShipRange)) Bool
+    (and (betweenInt (shipCapacity s) (shipCapacityD sr)) (betweenLoc (shipLoc s) (shipLocD sr)))
+)
+
+(define-fun atLeast ((s Ship)) Bool
+    (> (shipCapacity s) 50)
+)
+
+(define-fun subsetLoc ((s1 LocRange) (s2 LocRange)) Bool
+    (and (subsetInt (xD s1) (xD s2)) (subsetInt (yD s1) (yD s2)))
+)
+
+(define-fun subsetShip ((s1 ShipRange) (s2 ShipRange)) Bool
+    (and (subsetInt (shipCapacityD s1) (shipCapacityD s2)) (subsetLoc (shipLocD s1) (shipLocD s2)))
+)
+
+(define-fun max ((x Int) (y Int)) Int
+ (ite (>= x y) x y)
+)
+
+(define-fun min ((x Int) (y Int)) Int
+ (ite (<= x y) x y)
+)
+
+
+(synth-fun f ((secret Ship) (prior ShipRange) (response Bool)) ShipRange
+)
+
+(declare-var secret Ship)
+(declare-var prior ShipRange)
+(declare-var response Bool)
+
+(constraint (=> (betweenShip secret prior)
+ (=> (betweenShip secret (f secret prior response)) 
+         (= response 
+            (and (atLeast secret) 
+                 (subsetShip (f secret prior response) prior))))
+))
+
+(check-synth)