Disable filtering of shapes in sygus-rcons pool. (#7922)

This PR disables filtering of enumerated shapes in the pool of the Sygus reconstruction algorithm.

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index bd71de283f422dcd1bdda003082893042a8ed7c8..01454786a04980e0e88544916e0e3f45b1ecd079 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -457,20 +457,9 @@ bool SygusReconstruct::notify(Node s,
                               std::vector<Node>& vars,
                               std::vector<Node>& subs)
 {
-  for (size_t i = 0; i < vars.size(); ++i)
-  {
-    // We consider sygus variables as ground terms. So, if they are not equal to
-    // their substitution, then s is not matchable with n and we try the next
-    // term s. Example: If s = (+ z x) and n = (+ z y), then s is not matchable
-    // with n and we return true
-    if (d_sygusVars.find(vars[i]) != d_sygusVars.cend() && vars[i] != subs[i])
-    {
-      return true;
-    }
-  }
-  // Note: false here means that we finally found an s that is matchable with n,
-  // so we should not add n to the pool
-  return false;
+  // If we are too aggressive in filtering enumerated shapes, we may miss some
+  // that speedup reconstruction time. So, for now, we disable filtering.
+  return true;
 }
 
 void SygusReconstruct::clear()

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index de10b76ea225e1863d90708c3ff5b904e7464992..dca68844f7f75e65e1c5859f7e5c0aa5473b56bb 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -94,7 +94,7 @@ using NodePairMap = std::unordered_map<Node, Node>;
  *       TermsToRecons'' = {}
  *       for each subfield type T of T0
  *         for each t in TermsToRecons'[T]
- *           TermsToRecons'[T] += t
+ *           TermsToRecons[T] += t
  *           for each s[zs] in Pool[T]
  *             TermsToRecons'' += matchNewObs(t, s[zs])
  *         TermsToRecons' = TermsToRecons''
@@ -109,7 +109,7 @@ using NodePairMap = std::unordered_map<Node, Node>;
  *     Sub = {} // substitution map from zs to corresponding new vars ks
  *     for each (z, st) in {zs -> sts}
  *       // let X be the theory the solver is invoked with
- *       if exists (k, ts) in Obs s.t. !=_X ts[0] = st
+ *       if exists (k, ts) in Obs s.t. |=_X ts[0] = st
  *         ts += st
  *         Sub[z] = k
  *       else

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8b068aa3e83179da890d80e7abdb33c0a3c13dea..9183d24e723437406127104b75949815070282aa 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2750,6 +2750,7 @@ set(regress_2_tests
   regress2/sygus/min_IC_1.sy
   regress2/sygus/mpg_guard1-dd.sy
   regress2/sygus/multi-udiv.sy
+  regress2/sygus/no-bad-filter.sy
   regress2/sygus/no-syntax-test-no-si.sy
   regress2/sygus/pbe_bvurem.sy
   regress2/sygus/process-10-vars-2fun.sy

diff --git a/test/regress/regress2/sygus/no-bad-filter.sy b/test/regress/regress2/sygus/no-bad-filter.sy
new file mode 100644 (file)
index 0000000..4e7c350
--- /dev/null
+++ b/test/regress/regress2/sygus/no-bad-filter.sy
@@ -0,0 +1,34 @@
+; COMMAND-LINE: --sygus-out=status --sygus-si=all
+; EXPECT: unsat
+
+; This regression ensures that we are not too aggressive in filtering
+; enumerated shapes in the pool.
+
+(set-logic SLIA)
+
+(synth-fun f ((x String) (y String)) String
+  ((Start String) (StartInt Int) (StartBool Bool) (ConstString String))
+  ((Start String (ConstString x y
+                  (str.++ Start Start)
+                  (str.substr Start StartInt StartInt)
+                  (str.replace_all Start Start Start)
+                  (str.from_code StartInt)
+                  (str.from_int StartInt)
+                  (ite StartBool Start Start)))
+   (StartInt Int (0 1 (str.len Start)
+                  (str.indexof Start Start StartInt)
+                  (str.to_code Start)
+                  (str.to_int Start)))
+   (StartBool Bool ((and StartBool StartBool)
+                    (str.<= Start Start)
+                    (str.is_digit Start)
+                    (not StartBool)
+                    (<= StartInt StartInt)))
+   (ConstString String ("" "0" "1" "a" "b" (Constant String)))))
+
+(declare-var x String)
+(declare-var y String)
+
+(constraint (= (f x y) (str.at y (str.indexof y "a" (str.len x)))))
+
+(check-synth)