diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-24 15:03:28 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-09-24 15:03:28 +0000 |
commit | 353c6d5c3770365f0dffcbdf697199bed156cf50 (patch) | |
tree | e8a019cf24b3a4dd2b4eb458cbe066164b6eddee /test/regress | |
parent | bb0fc300c810f68f1e901413272c6658e31d60f9 (diff) |
basic union find for bitvectors
Diffstat (limited to 'test/regress')
18 files changed, 487 insertions, 35 deletions
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 0624c00f1..5b8e6d7d3 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -4,41 +4,45 @@ TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - concat-merge-0.smt \ - concat-merge-1.smt \ - concat-merge-2.smt \ - concat-merge-3.smt \ - extract-concat-0.smt \ - extract-concat-1.smt \ - extract-concat-2.smt \ - extract-concat-3.smt \ - extract-concat-4.smt \ - extract-concat-5.smt \ - extract-concat-6.smt \ - extract-concat-7.smt \ - extract-concat-8.smt \ - extract-concat-9.smt \ - extract-concat-10.smt \ - extract-concat-11.smt \ - extract-constant.smt \ - extract-extract-0.smt \ - extract-extract-1.smt \ - extract-extract-2.smt \ - extract-extract-3.smt \ - extract-extract-4.smt \ - extract-extract-5.smt \ - extract-extract-6.smt \ - extract-extract-7.smt \ - extract-extract-8.smt \ - extract-extract-9.smt \ - extract-extract-10.smt \ - extract-extract-11.smt \ - extract-whole-0.smt \ - extract-whole-1.smt \ - extract-whole-2.smt \ - extract-whole-3.smt \ - extract-whole-4.smt - + concat-merge-0.smt \ + concat-merge-1.smt \ + concat-merge-2.smt \ + concat-merge-3.smt \ + extract-concat-0.smt \ + extract-concat-1.smt \ + extract-concat-2.smt \ + extract-concat-3.smt \ + extract-concat-4.smt \ + extract-concat-5.smt \ + extract-concat-6.smt \ + extract-concat-7.smt \ + extract-concat-8.smt \ + extract-concat-9.smt \ + extract-concat-10.smt \ + extract-concat-11.smt \ + extract-constant.smt \ + extract-extract-0.smt \ + extract-extract-1.smt \ + extract-extract-2.smt \ + extract-extract-3.smt \ + extract-extract-4.smt \ + extract-extract-5.smt \ + extract-extract-6.smt \ + extract-extract-7.smt \ + extract-extract-8.smt \ + extract-extract-9.smt \ + extract-extract-10.smt \ + extract-extract-11.smt \ + extract-whole-0.smt \ + extract-whole-1.smt \ + extract-whole-2.smt \ + extract-whole-3.smt \ + extract-whole-4.smt \ + equality-00.smt \ + equality-01.smt \ + equality-02.smt \ + bv_eq_diamond10.smt + EXTRA_DIST = $(TESTS) # synonyms for "check" diff --git a/test/regress/regress0/bv/core/bv_eq_diamond10.smt b/test/regress/regress0/bv/core/bv_eq_diamond10.smt new file mode 100644 index 000000000..6d8042512 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond10.smt @@ -0,0 +1,33 @@ +(benchmark eq_diamond10 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(not (= x0 x9)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond11.smt b/test/regress/regress0/bv/core/bv_eq_diamond11.smt new file mode 100644 index 000000000..cf9dccf07 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond11.smt @@ -0,0 +1,35 @@ +(benchmark eq_diamond11 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(not (= x0 x10)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond12.smt b/test/regress/regress0/bv/core/bv_eq_diamond12.smt new file mode 100644 index 000000000..97f7159c7 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond12.smt @@ -0,0 +1,37 @@ +(benchmark eq_diamond12 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(not (= x0 x11)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond13.smt b/test/regress/regress0/bv/core/bv_eq_diamond13.smt new file mode 100644 index 000000000..9e25875e1 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond13.smt @@ -0,0 +1,39 @@ +(benchmark eq_diamond13 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(not (= x0 x12)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond14.smt b/test/regress/regress0/bv/core/bv_eq_diamond14.smt new file mode 100644 index 000000000..9eae02e30 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond14.smt @@ -0,0 +1,41 @@ +(benchmark eq_diamond14 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(not (= x0 x13)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond15.smt b/test/regress/regress0/bv/core/bv_eq_diamond15.smt new file mode 100644 index 000000000..ed28883a5 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond15.smt @@ -0,0 +1,43 @@ +(benchmark eq_diamond15 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(not (= x0 x14)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond16.smt b/test/regress/regress0/bv/core/bv_eq_diamond16.smt new file mode 100644 index 000000000..4e81c3c31 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond16.smt @@ -0,0 +1,45 @@ +(benchmark eq_diamond16 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) +(not (= x0 x15)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond17.smt b/test/regress/regress0/bv/core/bv_eq_diamond17.smt new file mode 100644 index 000000000..b65e035e5 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond17.smt @@ -0,0 +1,47 @@ +(benchmark eq_diamond17 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32]) +(x16 BitVec[32]) (y16 BitVec[32]) (z16 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) +(or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) +(not (= x0 x16)))) diff --git a/test/regress/regress0/bv/core/equality-00.cvc b/test/regress/regress0/bv/core/equality-00.cvc new file mode 100644 index 000000000..e02c616ad --- /dev/null +++ b/test/regress/regress0/bv/core/equality-00.cvc @@ -0,0 +1,4 @@ +x, y, z : BITVECTOR(32); +ASSERT(x = y); +ASSERT(y = z); +QUERY(x = z);
\ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-00.smt b/test/regress/regress0/bv/core/equality-00.smt new file mode 100644 index 000000000..dabdae5f9 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-00.smt @@ -0,0 +1,10 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :extrafuns ((z BitVec[32])) + :assumption (= x y) + :assumption (= y z) + :formula (not (= x z)) +) diff --git a/test/regress/regress0/bv/core/equality-01.cvc b/test/regress/regress0/bv/core/equality-01.cvc new file mode 100644 index 000000000..e56af23dd --- /dev/null +++ b/test/regress/regress0/bv/core/equality-01.cvc @@ -0,0 +1,5 @@ +x, y, z, w: BITVECTOR(32); +ASSERT(x = y); +ASSERT(y = z); +ASSERT(z = w); +QUERY(x = w);
\ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-01.smt b/test/regress/regress0/bv/core/equality-01.smt new file mode 100644 index 000000000..48506d2b9 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-01.smt @@ -0,0 +1,12 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :extrafuns ((z BitVec[32])) + :extrafuns ((w BitVec[32])) + :assumption (= x y) + :assumption (= y z) + :assumption (= z w) + :formula (not (= x w)) +) diff --git a/test/regress/regress0/bv/core/equality-02.cvc b/test/regress/regress0/bv/core/equality-02.cvc new file mode 100644 index 000000000..e8f51d61a --- /dev/null +++ b/test/regress/regress0/bv/core/equality-02.cvc @@ -0,0 +1,15 @@ +x0, x1, x2, x3 : BITVECTOR(32); +y0, y1, y2, y3 : BITVECTOR(32); + +ASSERT (x0 = x1); +ASSERT (x1 = x2); +ASSERT (x2 = x3); + +ASSERT (y0 = y1); +ASSERT (y1 = y2); +ASSERT (y2 = y3); + +ASSERT (x0 = y0); + +QUERY (x3 = y3); + diff --git a/test/regress/regress0/bv/core/equality-02.smt b/test/regress/regress0/bv/core/equality-02.smt new file mode 100644 index 000000000..ee011ceb4 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-02.smt @@ -0,0 +1,20 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x0 BitVec[32])) + :extrafuns ((x1 BitVec[32])) + :extrafuns ((x2 BitVec[32])) + :extrafuns ((x3 BitVec[32])) + :extrafuns ((y0 BitVec[32])) + :extrafuns ((y1 BitVec[32])) + :extrafuns ((y2 BitVec[32])) + :extrafuns ((y3 BitVec[32])) + :assumption (= x0 x1) + :assumption (= x1 x2) + :assumption (= x2 x3) + :assumption (= y0 y1) + :assumption (= y1 y2) + :assumption (= y2 y3) + :assumption (= x0 y0) + :formula (not (= x3 y3)) +) diff --git a/test/regress/regress0/bv/core/equality-03.cvc b/test/regress/regress0/bv/core/equality-03.cvc new file mode 100644 index 000000000..d2f18682c --- /dev/null +++ b/test/regress/regress0/bv/core/equality-03.cvc @@ -0,0 +1,10 @@ +x0, x1, x2: BITVECTOR(32); +y0, y1, y2: BITVECTOR(32); +a0, a1, a2, a3 : BITVECTOR(32); + +ASSERT (a0 = x0 AND x0 = a1) XOR (a0 = y0 AND y0 = a1); +ASSERT (a1 = x1 AND x1 = a2) XOR (a1 = y1 AND y1 = a2); +ASSERT (a2 = x2 AND x2 = a3) XOR (a2 = y2 AND y2 = a3); + +QUERY (a0 = a3); + diff --git a/test/regress/regress0/bv/core/equality-03.smt b/test/regress/regress0/bv/core/equality-03.smt new file mode 100644 index 000000000..4141c7293 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-03.smt @@ -0,0 +1,27 @@ +(benchmark B_ + :source { +Source unknown +} + :status unknown + :difficulty { unknown } + :category { unknown } + :logic QF_BV + :extrafuns ((x0 BitVec[32])) + :extrafuns ((x1 BitVec[32])) + :extrafuns ((x2 BitVec[32])) + :extrafuns ((y0 BitVec[32])) + :extrafuns ((y1 BitVec[32])) + :extrafuns ((y2 BitVec[32])) + :extrafuns ((a0 BitVec[32])) + :extrafuns ((a1 BitVec[32])) + :extrafuns ((a2 BitVec[32])) + :extrafuns ((a3 BitVec[32])) + :assumption +(xor (and (= a0 x0) (= x0 a1)) (and (= a0 y0) (= y0 a1))) + :assumption +(xor (and (= a1 x1) (= x1 a2)) (and (= a1 y1) (= y1 a2))) + :assumption +(xor (and (= a2 x2) (= x2 a3)) (and (= a2 y2) (= y2 a3))) + :formula +(not (= a0 a3)) +) diff --git a/test/regress/regress0/bv/core/equality-04.smt b/test/regress/regress0/bv/core/equality-04.smt new file mode 100644 index 000000000..78adf0477 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-04.smt @@ -0,0 +1,25 @@ +(benchmark eq_diamond10 +:status unsat +:logic QF_BV +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(not (= x0 x9)))) |