From 4975ae6cd117f6103ada4ccca329b1e348583ce0 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 11 Jan 2022 15:58:17 -0600
Subject: [PATCH] Disable filtering of shapes in sygus-rcons pool. (#7922)

This PR disables filtering of enumerated shapes in the pool of the Sygus reconstruction algorithm.
---
 .../quantifiers/sygus/sygus_reconstruct.cpp   | 17 ++--------
 .../quantifiers/sygus/sygus_reconstruct.h     |  4 +--
 test/regress/CMakeLists.txt                   |  1 +
 test/regress/regress2/sygus/no-bad-filter.sy  | 34 +++++++++++++++++++
 4 files changed, 40 insertions(+), 16 deletions(-)
 create mode 100644 test/regress/regress2/sygus/no-bad-filter.sy

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index bd71de283..01454786a 100644
--- 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 de10b76ea..dca68844f 100644
--- 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 8b068aa3e..9183d24e7 100644
--- 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
index 000000000..4e7c35033
--- /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)
-- 
2.30.2