From: Paul Meng Date: Tue, 30 Aug 2016 18:36:58 +0000 (-0500) Subject: added more benchmarks X-Git-Tag: cvc5-1.0.0~6036 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94504ecc81f13c6ed96d4c5bc0432ba3932efa91;p=cvc5.git added more benchmarks --- diff --git a/test/regress/regress0/sets/rels/addr_book.cvc b/test/regress/regress0/sets/rels/addr_book.cvc new file mode 100644 index 000000000..fbe782ab2 --- /dev/null +++ b/test/regress/regress0/sets/rels/addr_book.cvc @@ -0,0 +1,49 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom : TYPE; +AtomTup : TYPE = [Atom]; +AtomBinTup : TYPE = [Atom, Atom]; +AtomTerTup : TYPE = [Atom, Atom, Atom]; +Target: SET OF AtomTup; + +Name: SET OF AtomTup; +Addr: SET OF AtomTup; +Book: SET OF AtomTup; +names: SET OF AtomBinTup; +addr: SET OF AtomTerTup; + +b1: Atom; +b1_tup : AtomTup; +ASSERT b1_tup = TUPLE(b1); +ASSERT b1_tup IS_IN Book; + +b2: Atom; +b2_tup : AtomTup; +ASSERT b2_tup = TUPLE(b2); +ASSERT b2_tup IS_IN Book; + +b3: Atom; +b3_tup : AtomTup; +ASSERT b3_tup = TUPLE(b3); +ASSERT b3_tup IS_IN Book; + +n: Atom; +n_tup : AtomTup; +ASSERT n_tup = TUPLE(n); +ASSERT n_tup IS_IN Name; + +t: Atom; +t_tup : AtomTup; +ASSERT t_tup = TUPLE(t); +ASSERT t_tup IS_IN Target; + +ASSERT ((Book JOIN addr) JOIN Target) = Name; +ASSERT (Book JOIN names) = Name; +ASSERT (Name & Addr) = {}::SET OF AtomTup; + +ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; +ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup}; +ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup}; +ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr))); + +CHECKSAT; \ No newline at end of file diff --git a/test/regress/regress0/sets/rels/garbage_collect.cvc b/test/regress/regress0/sets/rels/garbage_collect.cvc new file mode 100644 index 000000000..dd5995c42 --- /dev/null +++ b/test/regress/regress0/sets/rels/garbage_collect.cvc @@ -0,0 +1,59 @@ +H_TYPE: TYPE; +H: TYPE = [H_TYPE]; +Obj: TYPE; +Obj_Tup: TYPE = [Obj]; +MARK_TYPE: TYPE = [H_TYPE, Obj]; +RELATE: TYPE = [Obj, Obj]; +REF_TYPE: TYPE = [H_TYPE, Obj, Obj]; + +% Symbols h0 to h3 are constants of type H that represents the system state; +h0: SET OF H; +h1: SET OF H; +h2: SET OF H; +h3: SET OF H; +s0: H_TYPE; +s1: H_TYPE; +s2: H_TYPE; +s3: H_TYPE; +ASSERT h0 = {TUPLE(s0)}; +ASSERT h1 = {TUPLE(s1)}; +ASSERT h2 = {TUPLE(s2)}; +ASSERT h3 = {TUPLE(s3)}; + +% ref ⊆ H × Obj × Obj represents references between objects in each state; +ref : SET OF REF_TYPE; + +% mark ⊆ H × Obj represents the marked objects in each state +mark: SET OF MARK_TYPE; + +empty_obj_set: SET OF Obj_Tup; +ASSERT empty_obj_set = {}:: SET OF Obj_Tup; + +% root and live are two constants of type Obj that represents objects; +root: Obj; +live: Obj; + +% The state transition (h0–h1) resets all the marks +ASSERT (h1 JOIN mark) = empty_obj_set; +ASSERT (h0 JOIN ref) <= (h1 JOIN ref); + +% (h1–h2) marks objects reachable from root +ASSERT FORALL (n : Obj) : ((root, n) IS_IN TCLOSURE(h1 JOIN ref)) + => (TUPLE(n) IS_IN (h2 JOIN mark)); +ASSERT (h1 JOIN ref) <= (h2 JOIN ref); + +% (h2–h3) sweeps references of non-marked objects + +ASSERT FORALL (n: Obj) : (NOT (TUPLE(n) IS_IN (h2 JOIN mark))) + => ({TUPLE(n)} JOIN (h3 JOIN ref)) = empty_obj_set; + +ASSERT FORALL (n: Obj) : (TUPLE(n) IS_IN (h2 JOIN mark)) + => ({TUPLE(n)} JOIN (h3 JOIN ref)) = ({TUPLE(n)} JOIN (h2 JOIN ref)); + +%The safety property is negated, thus it checks if +%in the final state, there is a live object that was originally reachable from root +%in the beginning state, but some of its references have been swept +ASSERT (root, live) IS_IN TCLOSURE(h0 JOIN ref); +ASSERT NOT (({TUPLE(live)} JOIN (h0 JOIN ref)) <= ({TUPLE(live)} JOIN (h3 JOIN ref))); + +CHECKSAT; \ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_join_1_1.cvc b/test/regress/regress0/sets/rels/rel_join_1_1.cvc index 3436bd707..75fc08387 100644 --- a/test/regress/regress0/sets/rels/rel_join_1_1.cvc +++ b/test/regress/regress0/sets/rels/rel_join_1_1.cvc @@ -26,6 +26,6 @@ ASSERT (4, 7) IS_IN y; ASSERT z IS_IN x; ASSERT zt IS_IN y; -ASSERT a IS_IN (x JOIN y); +ASSERT r = (x JOIN y); CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1_1.cvc b/test/regress/regress0/sets/rels/rel_product_1_1.cvc index 3e5280c19..9559b74e1 100644 --- a/test/regress/regress0/sets/rels/rel_product_1_1.cvc +++ b/test/regress/regress0/sets/rels/rel_product_1_1.cvc @@ -4,17 +4,18 @@ IntPair: TYPE = [INT, INT, INT]; IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; x : SET OF IntPair; y : SET OF IntPair; -r : SET OF IntPair; +r : SET OF IntTup; z : IntPair; ASSERT z = (1,2,3); zt : IntPair; ASSERT zt = (3,2,1); -v : IntTup; -ASSERT v = (1,2,3,3,2,1); + ASSERT z IS_IN x; ASSERT zt IS_IN y; -ASSERT v IS_IN (x PRODUCT y); +ASSERT (1,1,1,1,1,1) IS_IN r; +ASSERT r = (x PRODUCT y); + CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_10_1.cvc b/test/regress/regress0/sets/rels/rel_tc_10_1.cvc new file mode 100644 index 000000000..67c444070 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_10_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT a = c; +ASSERT a = d; +ASSERT (1, c) IS_IN x; +ASSERT (2, d) IS_IN x; +ASSERT (a, 5) IS_IN y; +ASSERT y = (TCLOSURE x); +ASSERT ((2, 5) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_11.cvc b/test/regress/regress0/sets/rels/rel_tc_11.cvc new file mode 100644 index 000000000..7edeb0efb --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_11.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntTup; +ASSERT (2, 3) IS_IN x; +ASSERT (5, 3) IS_IN x; +ASSERT (3, 9) IS_IN x; +ASSERT z = (x PRODUCT y); +ASSERT (1, 2, 3, 4) IS_IN z; +ASSERT NOT ((5, 9) IS_IN x); +ASSERT (3, 8) IS_IN y; +ASSERT y = (TCLOSURE x); +ASSERT NOT ((1, 2) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_2_1.cvc b/test/regress/regress0/sets/rels/rel_tc_2_1.cvc new file mode 100644 index 000000000..d5d42eaad --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_2_1.cvc @@ -0,0 +1,28 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + e: INT; + +a : IntPair; +ASSERT a = (1, e); + +d : IntPair; +ASSERT d = (e,5); + +ASSERT a IS_IN x; +ASSERT d IS_IN x; +ASSERT NOT ((1,1) IS_IN x); +ASSERT NOT ((1,2) IS_IN x); +ASSERT NOT ((1,3) IS_IN x); +ASSERT NOT ((1,4) IS_IN x); +ASSERT NOT ((1,5) IS_IN x); +ASSERT NOT ((1,6) IS_IN x); +ASSERT NOT ((1,7) IS_IN x); + +ASSERT y = TCLOSURE(x); + +ASSERT (1, 5) IS_IN y; + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_3.cvc b/test/regress/regress0/sets/rels/rel_tc_3.cvc index 79ba32448..39564c4cf 100644 --- a/test/regress/regress0/sets/rels/rel_tc_3.cvc +++ b/test/regress/regress0/sets/rels/rel_tc_3.cvc @@ -12,9 +12,11 @@ ASSERT (1, c) IS_IN x; ASSERT (1, d) IS_IN x; ASSERT (b, 1) IS_IN x; ASSERT (b = d); -ASSERT (2,3) IS_IN ((x JOIN x) JOIN x); -ASSERT NOT (2, 3) IS_IN (TRANSCLOSURE x); -ASSERT y = (TRANSCLOSURE x); +ASSERT (b > (d -1)); +ASSERT (b < (d+1)); +%ASSERT (2,3) IS_IN ((x JOIN x) JOIN x); +%ASSERT NOT (2, 3) IS_IN (TCLOSURE x); +ASSERT y = (TCLOSURE x); ASSERT NOT ((1, 1) IS_IN y); CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_3_1.cvc b/test/regress/regress0/sets/rels/rel_tc_3_1.cvc new file mode 100644 index 000000000..e48ba4eb6 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_3_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT (1, a) IS_IN x; +ASSERT (1, c) IS_IN x; +ASSERT (1, d) IS_IN x; +ASSERT (b, 1) IS_IN x; +ASSERT (b = d); + +ASSERT y = (TCLOSURE x); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_4.cvc b/test/regress/regress0/sets/rels/rel_tc_4.cvc new file mode 100644 index 000000000..decd38fe1 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_4.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT (1, a) IS_IN x; +ASSERT (1, c) IS_IN x; +ASSERT (1, d) IS_IN x; +ASSERT (b, 1) IS_IN x; +ASSERT (b = d); +ASSERT (2,b) IS_IN ((x JOIN x) JOIN x); +ASSERT NOT (2, 1) IS_IN (TCLOSURE x); + + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_4_1.cvc b/test/regress/regress0/sets/rels/rel_tc_4_1.cvc new file mode 100644 index 000000000..8ee75f7e9 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_4_1.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +ASSERT y = ((TCLOSURE x) JOIN x); +ASSERT NOT (y = TCLOSURE x); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_5_1.cvc b/test/regress/regress0/sets/rels/rel_tc_5_1.cvc new file mode 100644 index 000000000..fd9caeade --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_5_1.cvc @@ -0,0 +1,9 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = (TCLOSURE x); +ASSERT NOT ( y = ((x JOIN x) JOIN x)); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_6.cvc b/test/regress/regress0/sets/rels/rel_tc_6.cvc new file mode 100644 index 000000000..4570c5a8d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_6.cvc @@ -0,0 +1,9 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = (TCLOSURE x); +ASSERT NOT (((x JOIN x) JOIN x) <= y); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_7.cvc b/test/regress/regress0/sets/rels/rel_tc_7.cvc new file mode 100644 index 000000000..15c0510a6 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_7.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = ((TCLOSURE x) JOIN x); +ASSERT (1,2) IS_IN ((x JOIN x) JOIN x); +ASSERT NOT (y <= TCLOSURE x); + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_8.cvc b/test/regress/regress0/sets/rels/rel_tc_8.cvc new file mode 100644 index 000000000..9f5879c6d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_8.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +ASSERT (2, 2) IS_IN (TCLOSURE x); +ASSERT x = {}::SET OF IntPair; + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tc_9_1.cvc b/test/regress/regress0/sets/rels/rel_tc_9_1.cvc new file mode 100644 index 000000000..f884349b1 --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tc_9_1.cvc @@ -0,0 +1,23 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +w : SET OF IntPair; + +ASSERT z = (TCLOSURE x); +ASSERT w = (x JOIN y); +ASSERT (2, 2) IS_IN z; +ASSERT (0,3) IS_IN y; +ASSERT (-1,3) IS_IN y; +ASSERT (1,3) IS_IN y; +ASSERT (-2,3) IS_IN y; +ASSERT (2,3) IS_IN y; +ASSERT (3,3) IS_IN y; +ASSERT (4,3) IS_IN y; +ASSERT (5,3) IS_IN y; +ASSERT NOT (2, 3) IS_IN (x JOIN y); +ASSERT NOT (2,1) IS_IN x; + +CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc index 6da02ea2d..49fb87569 100644 --- a/test/regress/regress0/sets/rels/rel_transpose_0.cvc +++ b/test/regress/regress0/sets/rels/rel_transpose_0.cvc @@ -4,6 +4,7 @@ IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; +a: INT; z : IntPair; ASSERT z = (1,2); zt : IntPair; @@ -12,7 +13,6 @@ ASSERT zt = (2,1); ASSERT z IS_IN x; ASSERT NOT (zt IS_IN (TRANSPOSE x)); -ASSERT z IS_IN y; -ASSERT NOT (zt IS_IN (TRANSPOSE y)); +ASSERT y = (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 index 11653de04..fa6ee5069 100644 --- a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc +++ b/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc @@ -4,9 +4,11 @@ IntTup: TYPE = [INT, INT, INT]; x : SET OF IntTup; y : SET OF IntTup; z : IntTup; -ASSERT z = (1,2,3); +a: INT; +ASSERT z = (1,2,a); zt : IntTup; -ASSERT zt = (3,2,1); +ASSERT zt = (3,2,2); ASSERT z IS_IN x; ASSERT zt IS_IN (TRANSPOSE x); +ASSERT y = (TRANSPOSE x); CHECKSAT;