Optimizations and fixes for computing whether a type is finite (#2179)

2 files changed, 145 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index b005a3a67..aa896258f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1491,6 +1491,7 @@ REG1_TESTS = \
 	regress1/strings/username_checker_min.smt2 \
 	regress1/sygus/VC22_a.sy \
 	regress1/sygus/array_search_2.sy \
+	regress1/sygus/array_search_5-Q-easy.sy \
 	regress1/sygus/array_sum_2_5.sy \
 	regress1/sygus/cegar1.sy \
 	regress1/sygus/cegisunif-depth1.sy \
diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
new file mode 100644
index 000000000..e1f37d2cd
--- /dev/null
+++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
@@ -0,0 +1,144 @@
+; EXPECT: unsat
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+( set-logic LIA )
+( synth-fun findIdx  (         ( y1  Int )  ( y2  Int )  ( y3  Int )  ( y4  Int )  ( y5  Int )  ( k1  Int ) )  Int (
+  (Start  Int (    NT1
+    NT3
+    NT4
+    NT7
+    NT8
+    NT9
+    NT10
+    NT11
+    NT13
+    NT14
+))
+  (NT1  Int (    y5
+    k1
+    1
+    y2
+    0
+    y1
+    2
+    5
+    y4
+    4
+    y3
+    3
+))
+  (NT2  Bool (    (< NT1 NT1)
+    (> NT1 NT1)
+    (>= NT1 NT1)
+    (<= NT1 NT1)
+))
+  (NT3  Int (    (ite NT2 NT1 NT1)
+))
+  (NT4  Int (    (ite NT5 NT1 NT1)
+    (ite NT2 NT3 NT1)
+))
+  (NT5  Bool (    (< NT3 NT1)
+    (<= NT3 NT1)
+    (>= NT3 NT1)
+    (> NT3 NT1)
+))
+  (NT6  Bool (    (<= NT4 NT1)
+    (> NT4 NT1)
+    (<= NT3 NT3)
+    (> NT3 NT3)
+    (>= NT4 NT1)
+    (< NT4 NT1)
+    (< NT3 NT3)
+    (>= NT3 NT3)
+))
+  (NT7  Int (    (ite NT6 NT1 NT1)
+    (ite NT2 NT4 NT1)
+))
+  (NT8  Int (    (ite NT2 NT7 NT1)
+    (ite NT5 NT4 NT1)
+    (ite NT15 NT1 NT1)
+    (ite NT5 NT1 NT4)
+))
+  (NT9  Int (    (ite NT2 NT8 NT1)
+    (ite NT12 NT1 NT1)
+    (ite NT6 NT1 NT4)
+    (ite NT6 NT4 NT1)
+    (ite NT5 NT7 NT1)
+))
+  (NT10  Int (    (ite NT5 NT8 NT1)
+    (ite NT16 NT1 NT1)
+    (ite NT2 NT9 NT1)
+    (ite NT6 NT7 NT1)
+    (ite NT5 NT4 NT4)
+))
+  (NT11  Int (    (ite NT6 NT8 NT1)
+    (ite NT2 NT10 NT1)
+    (ite NT5 NT9 NT1)
+    (ite NT17 NT1 NT1)
+    (ite NT6 NT4 NT4)
+))
+  (NT12  Bool (    (< NT4 NT4)
+    (> NT4 NT4)
+    (<= NT8 NT1)
+    (< NT8 NT1)
+    (<= NT4 NT4)
+    (> NT8 NT1)
+    (>= NT8 NT1)
+    (>= NT4 NT4)
+))
+  (NT13  Int (    (ite NT18 NT1 NT1)
+    (ite NT12 NT7 NT1)
+    (ite NT5 NT10 NT1)
+    (ite NT6 NT9 NT1)
+    (ite NT12 NT1 NT7)
+    (ite NT2 NT11 NT1)
+))
+  (NT14  Int (    (ite NT12 NT1 NT8)
+    (ite NT6 NT10 NT1)
+    (ite NT5 NT11 NT1)
+    (ite NT19 NT1 NT1)
+    (ite NT12 NT8 NT1)
+    (ite NT2 NT13 NT1)
+))
+  (NT15  Bool (    (>= NT7 NT1)
+    (< NT7 NT1)
+    (> NT7 NT1)
+    (<= NT7 NT1)
+))
+  (NT16  Bool (    (< NT9 NT1)
+    (>= NT9 NT1)
+    (> NT9 NT1)
+    (<= NT9 NT1)
+))
+  (NT17  Bool (    (< NT7 NT7)
+    (<= NT10 NT1)
+    (>= NT10 NT1)
+    (> NT10 NT1)
+    (< NT10 NT1)
+    (> NT7 NT7)
+    (>= NT7 NT7)
+    (<= NT7 NT7)
+))
+  (NT18  Bool (    (< NT11 NT1)
+    (> NT11 NT1)
+    (>= NT11 NT1)
+    (<= NT11 NT1)
+))
+  (NT19  Bool (    (>= NT13 NT1)
+    (>= NT8 NT8)
+    (< NT13 NT1)
+    (> NT13 NT1)
+    (< NT8 NT8)
+    (> NT8 NT8)
+    (<= NT8 NT8)
+    (<= NT13 NT1)
+))
+))
+  ( declare-var x1  Int )
+  ( declare-var x2  Int )
+  ( declare-var x3  Int )
+  ( declare-var x4  Int )
+  ( declare-var x5  Int )
+  ( declare-var k  Int )
+  ( constraint  ( =>     ( and     ( <     x1  x2 )  ( and     ( <     x2  x3 )  ( and     ( <     x3  x4 )  ( <     x4  x5 ) ) ) )  ( =>     ( <     k  x1 )  ( =     ( findIdx         x1  x2  x3  x4  x5  k )   0 ) ) ) )
+  ( check-synth )
+