diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-02-17 15:01:40 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-02-17 15:01:40 -0600 |
commit | eea4ce60a90e6807b008b430e39f16dcb263c8a6 (patch) | |
tree | 560c77098d5b37f3610375b043d614220b10e9e2 /test/regress/regress0/sets | |
parent | 464e5839579ebe43eef8f6ab9a05766056ab0896 (diff) |
added rules for join and transpose operators
added more benchmarks
Diffstat (limited to 'test/regress/regress0/sets')
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel.cvc | 20 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join.cvc | 26 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_0.cvc | 25 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_0_1.cvc | 26 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_1.cvc | 31 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_1_1.cvc | 31 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_2.cvc | 20 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_join_2_1.cvc | 20 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_transpose.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_transpose_0.cvc | 14 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_transpose_1.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/sets/rels/rel_transpose_1_1.cvc | 12 |
13 files changed, 230 insertions, 22 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index d694d553b..5069d061e 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -39,7 +39,6 @@ TESTS = \ mar2014/smaller.smt2 \ mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \ - rels/rel.cvc \ copy_check_heap_access_33_4.smt2 \ cvc-sample.cvc \ emptyset.smt2 \ @@ -84,4 +83,4 @@ regress regress0 test: check # do nothing in this subdir .PHONY: regress1 regress2 regress3 -regress1 regress2 regress3: +regress1 regress2 regress3:
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel.cvc b/test/regress/regress0/sets/rels/rel.cvc deleted file mode 100644 index 27eb43b9f..000000000 --- a/test/regress/regress0/sets/rels/rel.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -m: SET OF INT; -a: IntPair; -b: INT; - -ASSERT a IS_IN (y JOIN z); -ASSERT (y PRODUCT x) = (y PRODUCT z); -ASSERT x = ((y JOIN z) JOIN x); - -ASSERT x = y | z; -ASSERT x = y & z; -ASSERT y = y - z; -ASSERT z = (TRANSPOSE z); -ASSERT z = x | y; -CHECKSAT TRUE; diff --git a/test/regress/regress0/sets/rels/rel_join.cvc b/test/regress/regress0/sets/rels/rel_join.cvc new file mode 100644 index 000000000..7cce736f5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join.cvc @@ -0,0 +1,26 @@ +% 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_join_0.cvc b/test/regress/regress0/sets/rels/rel_join_0.cvc new file mode 100644 index 000000000..a251218c6 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0.cvc @@ -0,0 +1,25 @@ +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_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc new file mode 100644 index 000000000..70e35164a --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +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 a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1.cvc b/test/regress/regress0/sets/rels/rel_join_1.cvc new file mode 100644 index 000000000..c8921afb9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1.cvc @@ -0,0 +1,31 @@ +% 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 (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_1_1.cvc b/test/regress/regress0/sets/rels/rel_join_1_1.cvc new file mode 100644 index 000000000..3436bd707 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_1_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: sat +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 (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2.cvc b/test/regress/regress0/sets/rels/rel_join_2.cvc new file mode 100644 index 000000000..cac7ce84d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_join_2_1.cvc new file mode 100644 index 000000000..3e27b9cc5 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_join_2_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT 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_transpose.cvc new file mode 100644 index 000000000..10644d794 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +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)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc new file mode 100644 index 000000000..d06528fd2 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_0.cvc @@ -0,0 +1,14 @@ +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)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1.cvc new file mode 100644 index 000000000..bdcf31bb8 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc new file mode 100644 index 000000000..11653de04 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT zt IS_IN (TRANSPOSE x); +CHECKSAT; |