diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-21 09:19:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-21 09:19:31 -0500 |
commit | 0d12fcbb5f1c047f951a69aa6ef4ae127f499312 (patch) | |
tree | d177dd93a13a8ae4ac5c9a22ab8c5aa97537d19d /test | |
parent | 585d2ac394e99a155ed40aa2da2fb550ff60fc7b (diff) |
Optimizations and fixes for computing whether a type is finite (#2179)
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress1/sygus/array_search_5-Q-easy.sy | 144 |
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 ) + |