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.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c35c29610d57becb80067454c97d74a0e1eaa0f..1e21abc47266e785e37a8deb515cdd1fe073b6cb 100644 (file)
--- 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 e41bef01507cf57133d7b43bcba238bafb69c689..33d143a36ed36202f1d84fb57f073b73fbdb2f06 100644 (file)
--- 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 7ba3c97589b9c96d67272278991b3254a686ffcb..eb8102856d9f294ef007117f21952fdc57a01baa 100644 (file)
--- 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 80f4af98424720e41c4dd126e770b74456088715..9c43e8b51d9662cffa9f185e5b0c27eb7532e11a 100644 (file)
--- 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 8909bfc0668528804c15b6279a96aa33ce9464f0..852734772d2dc9318f4988ed6468b2f1ff3e1ea6 100644 (file)
--- 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 (file)
index 0000000..4b08a93
--- /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)