diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/rels/Makefile.am | 12 | ||||
-rw-r--r-- | test/regress/regress0/rels/iden_0.cvc | 28 | ||||
-rw-r--r-- | test/regress/regress0/rels/iden_1.cvc | 18 | ||||
-rw-r--r-- | test/regress/regress0/rels/iden_1_1.cvc | 21 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0.cvc | 33 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0_1.cvc | 35 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0_2.cvc | 38 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1.cvc | 20 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1_1.cvc | 21 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2.cvc | 33 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 24 |
11 files changed, 282 insertions, 1 deletions
diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index bb9c49298..d1c035371 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -102,7 +102,17 @@ TESTS = \ set-strat.cvc \ rel_tc_8.cvc \ atom_univ2.cvc \ - rels-sharing-simp.cvc + rels-sharing-simp.cvc \ + iden_0.cvc \ + iden_1_1.cvc \ + iden_1.cvc \ + joinImg_0_1.cvc \ + joinImg_0_2.cvc \ + joinImg_0.cvc \ + joinImg_1_1.cvc \ + joinImg_1.cvc \ + joinImg_2_1.cvc \ + joinImg_2.cvc # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/rels/iden_0.cvc b/test/regress/regress0/rels/iden_0.cvc new file mode 100644 index 000000000..4c2693084 --- /dev/null +++ b/test/regress/regress0/rels/iden_0.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +id : SET OF IntPair; + +t : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT TUPLE(1) IS_IN t; +ASSERT TUPLE(2) IS_IN t; +ASSERT z IS_IN x; +ASSERT zt IS_IN x; +ASSERT v IS_IN x; +ASSERT a IS_IN x; +ASSERT id = IDEN(t); +ASSERT NOT ((1, 1) IS_IN (id & x)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/iden_1.cvc b/test/regress/regress0/rels/iden_1.cvc new file mode 100644 index 000000000..f73700e88 --- /dev/null +++ b/test/regress/regress0/rels/iden_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom:TYPE; +AtomPair: TYPE = [Atom, Atom]; +x : SET OF AtomPair; +t : SET OF [Atom]; +univ : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +ASSERT univ = UNIVERSE::SET OF [Atom]; +ASSERT (a, b) IS_IN x; +ASSERT (c, d) IS_IN x; +ASSERT NOT(a = b); +ASSERT IDEN(x JOIN univ) = x; +CHECKSAT; diff --git a/test/regress/regress0/rels/iden_1_1.cvc b/test/regress/regress0/rels/iden_1_1.cvc new file mode 100644 index 000000000..d118f15dd --- /dev/null +++ b/test/regress/regress0/rels/iden_1_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom:TYPE; +AtomPair: TYPE = [Atom, Atom]; +x : SET OF AtomPair; +t : SET OF [Atom]; +univ : SET OF [Atom]; +univ2 : SET OF [Atom,Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +ASSERT univ = UNIVERSE::SET OF [Atom]; +ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom]; +ASSERT univ2 = (univ PRODUCT univ); +ASSERT (a, b) IS_IN x; +ASSERT (c, d) IS_IN x; +ASSERT NOT(a = b); +ASSERT IDEN(univ) <= x; +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc new file mode 100644 index 000000000..e36c6a647 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0.cvc @@ -0,0 +1,33 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); + +ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); + +ASSERT NOT(TUPLE(1) IS_IN (x JOIN_IMAGE 2)); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(1) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc new file mode 100644 index 000000000..602c4fe3f --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0_1.cvc @@ -0,0 +1,35 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; +u : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); +b: INT; + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); + +ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); + +ASSERT u = (x JOIN_IMAGE 1); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_0_2.cvc b/test/regress/regress0/rels/joinImg_0_2.cvc new file mode 100644 index 000000000..f71069217 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_0_2.cvc @@ -0,0 +1,38 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; +u : SET OF [INT]; +univ : SET OF [INT]; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +s : IntPair; +ASSERT s = (1,1); +a : IntPair; +ASSERT a = (1,5); +b: INT; + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); +ASSERT univ = (x JOIN_IMAGE 0); +ASSERT TUPLE(100) IS_IN t; + +ASSERT NOT (TUPLE(3) IS_IN univ); + +ASSERT u = (x JOIN_IMAGE 1); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc new file mode 100644 index 000000000..47e57c1fb --- /dev/null +++ b/test/regress/regress0/rels/joinImg_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT x = {(b, c), (d, e), (c, e)}; +ASSERT NOT(a = b); + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc new file mode 100644 index 000000000..a7927f7e2 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_1_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT t = (x JOIN_IMAGE 2); +ASSERT x = {(b, c), (d, e), (c, e)}; +ASSERT TUPLE(c) IS_IN t; + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc new file mode 100644 index 000000000..bbf57629b --- /dev/null +++ b/test/regress/regress0/rels/joinImg_2.cvc @@ -0,0 +1,33 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; +f : Atom; +g : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3); +%ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)}; +ASSERT (a, f) IS_IN x; +ASSERT (a, f) IS_IN y; +ASSERT x = y; + + + +ASSERT NOT(a = b); + +ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2)); +ASSERT f = d; + +CHECKSAT; diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc new file mode 100644 index 000000000..b38bfab06 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_2_1.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +x : SET OF [Atom, Atom]; +y : SET OF [Atom, Atom]; +r : SET OF [Atom, Atom]; + +t : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +e : Atom; +f : Atom; +g : Atom; + +ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); +ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1); +ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT x = {(f, g), (b, c), (d, e), (c, e)}; +ASSERT (NOT(a = b)) OR (NOT(a = f)); + +CHECKSAT;
\ No newline at end of file |