diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-03-10 14:34:26 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-03-10 14:34:26 -0600 |
commit | 378a4df93162fe8e673f5cff42f38c20a872a646 (patch) | |
tree | 16d371cdce0a9d94903a2cd210f22797169ab73e /test | |
parent | 7d9fe09b55eb7b9cf319594f163d1b57fc78c272 (diff) |
fixed the transpose-occur rule
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/sets/rels/rel_complex_1.cvc | 34 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_complex_3.cvc | 49 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_complex_4.cvc | 52 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join.cvc | 26 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_6.cvc (renamed from test/regress/regress0/sets/rels/rel_transpose.cvc) | 13 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_transpose_2.cvc | 12 |
6 files changed, 108 insertions, 78 deletions
diff --git a/test/regress/regress0/sets/rels/rel_complex_1.cvc b/test/regress/regress0/sets/rels/rel_complex_1.cvc deleted file mode 100644 index 969d0d71c..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_1.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -w : SET OF IntTup; -z : SET OF IntTup; -r2 : SET OF IntPair; - -a : IntPair; -ASSERT a = (3,1); -ASSERT a IS_IN x; - -d : IntPair; -ASSERT d = (1,3); -ASSERT d IS_IN y; - -e : IntPair; -ASSERT e = (4,3); -ASSERT r = (x JOIN y); - -ASSERT TUPLE(1) IS_IN w; -ASSERT TUPLE(2) IS_IN z; -ASSERT r2 = (w PRODUCT z); - -ASSERT NOT (e IS_IN r); -%ASSERT e IS_IN r2; -ASSERT (r <= r2); -ASSERT NOT ((3,3) IS_IN r2); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_complex_3.cvc b/test/regress/regress0/sets/rels/rel_complex_3.cvc new file mode 100644 index 000000000..492c94432 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_3.cvc @@ -0,0 +1,49 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); + +e : IntPair; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_complex_4.cvc b/test/regress/regress0/sets/rels/rel_complex_4.cvc new file mode 100644 index 000000000..f473b00aa --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_complex_4.cvc @@ -0,0 +1,52 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +r : SET OF IntPair; +w : SET OF IntPair; + + +f : IntPair; +ASSERT f = (3,1); +ASSERT f IS_IN x; + +g : IntPair; +ASSERT g = (1,3); +ASSERT g IS_IN y; + +h : IntPair; +ASSERT h = (3,5); +ASSERT h IS_IN x; +ASSERT h IS_IN y; + +ASSERT r = (x JOIN y); +a:INT; +e : IntPair; +ASSERT e = (a,a); +ASSERT w = {e}; +ASSERT TRANSPOSE(w) <= y; + +ASSERT NOT (e IS_IN r); +ASSERT NOT(z = (x & y)); +ASSERT z = (x - y); +ASSERT x <= y; +ASSERT e IS_IN (r JOIN z); +ASSERT e IS_IN x; +ASSERT e IS_IN (x & y); +CHECKSAT TRUE; + + + + + + + + + + + + + + diff --git a/test/regress/regress0/sets/rels/rel_join.cvc b/test/regress/regress0/sets/rels/rel_join.cvc deleted file mode 100644 index 7cce736f5..000000000 --- a/test/regress/regress0/sets/rels/rel_join.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -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 (7, 5) IS_IN y; - -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -%ASSERT a IS_IN (x JOIN y); -%ASSERT NOT (v IS_IN (x JOIN y)); -ASSERT NOT (a IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose.cvc b/test/regress/regress0/sets/rels/rel_join_6.cvc index 10644d794..17318872f 100644 --- a/test/regress/regress0/sets/rels/rel_transpose.cvc +++ b/test/regress/regress0/sets/rels/rel_join_6.cvc @@ -3,10 +3,11 @@ OPTION "logic" "ALL_SUPPORTED"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; -z : IntPair; -ASSERT z = (1,2); -zt : IntPair; -ASSERT zt = (2,1); -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE x)); +r : SET OF IntPair; +ASSERT x = {(1,2), (3, 4)}; + +ASSERT y = (x JOIN {(2,1), (4,3)}); + +ASSERT NOT ((1,1) IS_IN y); + CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_2.cvc b/test/regress/regress0/sets/rels/rel_transpose_2.cvc deleted file mode 100644 index 15a035b58..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_2.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z : IntTup; -ASSERT z = (1); -zt : IntTup; -ASSERT zt = (1); -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE x)); -CHECKSAT; |