From: Paul Meng <baolmeng@gmail.com>
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;