diff options
Diffstat (limited to 'test')
78 files changed, 1 insertions, 3098 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index abb6c02b2..2f36cc188 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -86,4 +86,4 @@ regress regress0 test: check # do nothing in this subdir .PHONY: regress1 regress2 regress3 -regress1 regress2 regress3:
\ No newline at end of file +regress1 regress2 regress3: diff --git a/test/regress/regress0/sets/rels/addr_book_0.cvc b/test/regress/regress0/sets/rels/addr_book_0.cvc deleted file mode 100644 index fbe782ab2..000000000 --- a/test/regress/regress0/sets/rels/addr_book_0.cvc +++ /dev/null @@ -1,49 +0,0 @@ -% 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/addr_book_1.cvc b/test/regress/regress0/sets/rels/addr_book_1.cvc deleted file mode 100644 index 34176f274..000000000 --- a/test/regress/regress0/sets/rels/addr_book_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% 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; - -m: Atom; -m_tup : AtomTup; -ASSERT m_tup = TUPLE(m); -ASSERT m_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)}; -ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)}; -ASSERT NOT (({b1_tup} JOIN addr) = ({b3_tup} JOIN addr)); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/addr_book_1_1.cvc b/test/regress/regress0/sets/rels/addr_book_1_1.cvc deleted file mode 100644 index 74e29eaee..000000000 --- a/test/regress/regress0/sets/rels/addr_book_1_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% 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; - -m: Atom; -m_tup : AtomTup; -ASSERT m_tup = TUPLE(m); -ASSERT m_tup IS_IN Name; - -t: Atom; -t_tup : AtomTup; -ASSERT t_tup = TUPLE(t); -ASSERT t_tup IS_IN Target; - -ASSERT ({m_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; -ASSERT ({b2_tup} JOIN addr) = ({b1_tup} JOIN addr) | {(m,t)}; -ASSERT ({b3_tup} JOIN addr) = ({b2_tup} JOIN addr) - {(m,t)}; -ASSERT (({b1_tup} JOIN addr) = ({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 deleted file mode 100644 index dd5995c42..000000000 --- a/test/regress/regress0/sets/rels/garbage_collect.cvc +++ /dev/null @@ -1,59 +0,0 @@ -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_1tup_0.cvc b/test/regress/regress0/sets/rels/rel_1tup_0.cvc deleted file mode 100644 index 50d4defd5..000000000 --- a/test/regress/regress0/sets/rels/rel_1tup_0.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT]; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntTup; -z: SET OF IntTup; - -b : IntPair; -ASSERT b = (2, 1); -ASSERT b IS_IN x; - -a : IntTup; -ASSERT a = TUPLE(1); -ASSERT a IS_IN y; - -c : IntTup; -ASSERT c = TUPLE(2); - -ASSERT z = (x JOIN y); - -ASSERT NOT (c IS_IN z); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_complex_0.cvc b/test/regress/regress0/sets/rels/rel_complex_0.cvc deleted file mode 100644 index dcb753973..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_0.cvc +++ /dev/null @@ -1,31 +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 : SET OF INT; -f : INT; -g : INT; - -e : IntPair; -ASSERT e = (4, f); -ASSERT e IS_IN x; - -d : IntPair; -ASSERT d = (g,3); -ASSERT d IS_IN y; - - -ASSERT z = {f, g}; -ASSERT 0 = f - g; - - - -a : IntPair; -ASSERT a = (4,3); - -ASSERT r = (x JOIN y); - -ASSERT NOT (a IS_IN r); -CHECKSAT; 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 deleted file mode 100644 index 492c94432..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_3.cvc +++ /dev/null @@ -1,49 +0,0 @@ -% 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 deleted file mode 100644 index f473b00aa..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_4.cvc +++ /dev/null @@ -1,52 +0,0 @@ -% 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_complex_5.cvc b/test/regress/regress0/sets/rels/rel_complex_5.cvc deleted file mode 100644 index d64817187..000000000 --- a/test/regress/regress0/sets/rels/rel_complex_5.cvc +++ /dev/null @@ -1,55 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [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:IntTup; -ASSERT a = TUPLE(1); -e : IntPair; -ASSERT e = (1,1); - -ASSERT w = ({a} PRODUCT {a}); -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_conflict_0.cvc b/test/regress/regress0/sets/rels/rel_conflict_0.cvc deleted file mode 100644 index c1b82339f..000000000 --- a/test/regress/regress0/sets/rels/rel_conflict_0.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -e : IntPair; -ASSERT e = (4, 4); -ASSERT e IS_IN x; - -ASSERT NOT ((4, 4) IS_IN x); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_0.cvc b/test/regress/regress0/sets/rels/rel_join_0.cvc deleted file mode 100644 index 406b8d312..000000000 --- a/test/regress/regress0/sets/rels/rel_join_0.cvc +++ /dev/null @@ -1,24 +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 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 deleted file mode 100644 index a7fa7efb9..000000000 --- a/test/regress/regress0/sets/rels/rel_join_0_1.cvc +++ /dev/null @@ -1,27 +0,0 @@ -% 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 (4, 3) 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 deleted file mode 100644 index c8921afb9..000000000 --- a/test/regress/regress0/sets/rels/rel_join_1.cvc +++ /dev/null @@ -1,31 +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 (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 deleted file mode 100644 index 75fc08387..000000000 --- a/test/regress/regress0/sets/rels/rel_join_1_1.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% 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 r = (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 deleted file mode 100644 index cac7ce84d..000000000 --- a/test/regress/regress0/sets/rels/rel_join_2.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 deleted file mode 100644 index 3e27b9cc5..000000000 --- a/test/regress/regress0/sets/rels/rel_join_2_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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_join_3.cvc b/test/regress/regress0/sets/rels/rel_join_3.cvc deleted file mode 100644 index 6e190cecf..000000000 --- a/test/regress/regress0/sets/rels/rel_join_3.cvc +++ /dev/null @@ -1,29 +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 (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 r = (x JOIN y); -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT NOT (a IS_IN r); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_3_1.cvc b/test/regress/regress0/sets/rels/rel_join_3_1.cvc deleted file mode 100644 index d4e666c6e..000000000 --- a/test/regress/regress0/sets/rels/rel_join_3_1.cvc +++ /dev/null @@ -1,29 +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 (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 r = (x JOIN y); -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT a IS_IN r; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_4.cvc b/test/regress/regress0/sets/rels/rel_join_4.cvc deleted file mode 100644 index 030810f3d..000000000 --- a/test/regress/regress0/sets/rels/rel_join_4.cvc +++ /dev/null @@ -1,32 +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); - -b : IntPair; -ASSERT b = (7, 5); - -ASSERT (1, 7) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (3, 4) IS_IN x; - -ASSERT b IS_IN y; -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT r = (x JOIN y); -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT NOT (a IS_IN r); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_5.cvc b/test/regress/regress0/sets/rels/rel_join_5.cvc deleted file mode 100644 index 5209d8131..000000000 --- a/test/regress/regress0/sets/rels/rel_join_5.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; - -ASSERT (7, 1) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT (3, 4) IS_IN z; - -a : IntPair; -ASSERT a = (1,4); -ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); -ASSERT NOT (a IS_IN r); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_join_6.cvc b/test/regress/regress0/sets/rels/rel_join_6.cvc deleted file mode 100644 index 17318872f..000000000 --- a/test/regress/regress0/sets/rels/rel_join_6.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -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_join_7.cvc b/test/regress/regress0/sets/rels/rel_join_7.cvc deleted file mode 100644 index fff5b6efe..000000000 --- a/test/regress/regress0/sets/rels/rel_join_7.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; -w : 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 w = (r | (x JOIN y)); -ASSERT NOT (a IS_IN w); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_mix_0.cvc b/test/regress/regress0/sets/rels/rel_mix_0.cvc deleted file mode 100644 index 723a9b2e2..000000000 --- a/test/regress/regress0/sets/rels/rel_mix_0.cvc +++ /dev/null @@ -1,30 +0,0 @@ -% EXPECT: sat -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; - -d : IntPair; -ASSERT d = (1,3); -ASSERT (1,3) IS_IN y; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); - -ASSERT r = (x JOIN y); -ASSERT r2 = (w PRODUCT z); - -ASSERT NOT (e IS_IN r); -%ASSERT e IS_IN r2; -ASSERT NOT (r = r2); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_pressure_0.cvc b/test/regress/regress0/sets/rels/rel_pressure_0.cvc deleted file mode 100644 index 6cdf03600..000000000 --- a/test/regress/regress0/sets/rels/rel_pressure_0.cvc +++ /dev/null @@ -1,617 +0,0 @@ -% 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; - -a11 : IntPair; -ASSERT a11 = (1, 1); -ASSERT a11 IS_IN x; -a12 : IntPair; -ASSERT a12 = (1, 2); -ASSERT a12 IS_IN x; -a13 : IntPair; -ASSERT a13 = (1, 3); -ASSERT a13 IS_IN x; -a14 : IntPair; -ASSERT a14 = (1, 4); -ASSERT a14 IS_IN x; -a15 : IntPair; -ASSERT a15 = (1, 5); -ASSERT a15 IS_IN x; -a16 : IntPair; -ASSERT a16 = (1, 6); -ASSERT a16 IS_IN x; -a17 : IntPair; -ASSERT a17 = (1, 7); -ASSERT a17 IS_IN x; -a18 : IntPair; -ASSERT a18 = (1, 8); -ASSERT a18 IS_IN x; -a19 : IntPair; -ASSERT a19 = (1, 9); -ASSERT a19 IS_IN x; -a110 : IntPair; -ASSERT a110 = (1, 10); -ASSERT a110 IS_IN x; -a21 : IntPair; -ASSERT a21 = (2, 1); -ASSERT a21 IS_IN x; -a22 : IntPair; -ASSERT a22 = (2, 2); -ASSERT a22 IS_IN x; -a23 : IntPair; -ASSERT a23 = (2, 3); -ASSERT a23 IS_IN x; -a24 : IntPair; -ASSERT a24 = (2, 4); -ASSERT a24 IS_IN x; -a25 : IntPair; -ASSERT a25 = (2, 5); -ASSERT a25 IS_IN x; -a26 : IntPair; -ASSERT a26 = (2, 6); -ASSERT a26 IS_IN x; -a27 : IntPair; -ASSERT a27 = (2, 7); -ASSERT a27 IS_IN x; -a28 : IntPair; -ASSERT a28 = (2, 8); -ASSERT a28 IS_IN x; -a29 : IntPair; -ASSERT a29 = (2, 9); -ASSERT a29 IS_IN x; -a210 : IntPair; -ASSERT a210 = (2, 10); -ASSERT a210 IS_IN x; -a31 : IntPair; -ASSERT a31 = (3, 1); -ASSERT a31 IS_IN x; -a32 : IntPair; -ASSERT a32 = (3, 2); -ASSERT a32 IS_IN x; -a33 : IntPair; -ASSERT a33 = (3, 3); -ASSERT a33 IS_IN x; -a34 : IntPair; -ASSERT a34 = (3, 4); -ASSERT a34 IS_IN x; -a35 : IntPair; -ASSERT a35 = (3, 5); -ASSERT a35 IS_IN x; -a36 : IntPair; -ASSERT a36 = (3, 6); -ASSERT a36 IS_IN x; -a37 : IntPair; -ASSERT a37 = (3, 7); -ASSERT a37 IS_IN x; -a38 : IntPair; -ASSERT a38 = (3, 8); -ASSERT a38 IS_IN x; -a39 : IntPair; -ASSERT a39 = (3, 9); -ASSERT a39 IS_IN x; -a310 : IntPair; -ASSERT a310 = (3, 10); -ASSERT a310 IS_IN x; -a41 : IntPair; -ASSERT a41 = (4, 1); -ASSERT a41 IS_IN x; -a42 : IntPair; -ASSERT a42 = (4, 2); -ASSERT a42 IS_IN x; -a43 : IntPair; -ASSERT a43 = (4, 3); -ASSERT a43 IS_IN x; -a44 : IntPair; -ASSERT a44 = (4, 4); -ASSERT a44 IS_IN x; -a45 : IntPair; -ASSERT a45 = (4, 5); -ASSERT a45 IS_IN x; -a46 : IntPair; -ASSERT a46 = (4, 6); -ASSERT a46 IS_IN x; -a47 : IntPair; -ASSERT a47 = (4, 7); -ASSERT a47 IS_IN x; -a48 : IntPair; -ASSERT a48 = (4, 8); -ASSERT a48 IS_IN x; -a49 : IntPair; -ASSERT a49 = (4, 9); -ASSERT a49 IS_IN x; -a410 : IntPair; -ASSERT a410 = (4, 10); -ASSERT a410 IS_IN x; -a51 : IntPair; -ASSERT a51 = (5, 1); -ASSERT a51 IS_IN x; -a52 : IntPair; -ASSERT a52 = (5, 2); -ASSERT a52 IS_IN x; -a53 : IntPair; -ASSERT a53 = (5, 3); -ASSERT a53 IS_IN x; -a54 : IntPair; -ASSERT a54 = (5, 4); -ASSERT a54 IS_IN x; -a55 : IntPair; -ASSERT a55 = (5, 5); -ASSERT a55 IS_IN x; -a56 : IntPair; -ASSERT a56 = (5, 6); -ASSERT a56 IS_IN x; -a57 : IntPair; -ASSERT a57 = (5, 7); -ASSERT a57 IS_IN x; -a58 : IntPair; -ASSERT a58 = (5, 8); -ASSERT a58 IS_IN x; -a59 : IntPair; -ASSERT a59 = (5, 9); -ASSERT a59 IS_IN x; -a510 : IntPair; -ASSERT a510 = (5, 10); -ASSERT a510 IS_IN x; -a61 : IntPair; -ASSERT a61 = (6, 1); -ASSERT a61 IS_IN x; -a62 : IntPair; -ASSERT a62 = (6, 2); -ASSERT a62 IS_IN x; -a63 : IntPair; -ASSERT a63 = (6, 3); -ASSERT a63 IS_IN x; -a64 : IntPair; -ASSERT a64 = (6, 4); -ASSERT a64 IS_IN x; -a65 : IntPair; -ASSERT a65 = (6, 5); -ASSERT a65 IS_IN x; -a66 : IntPair; -ASSERT a66 = (6, 6); -ASSERT a66 IS_IN x; -a67 : IntPair; -ASSERT a67 = (6, 7); -ASSERT a67 IS_IN x; -a68 : IntPair; -ASSERT a68 = (6, 8); -ASSERT a68 IS_IN x; -a69 : IntPair; -ASSERT a69 = (6, 9); -ASSERT a69 IS_IN x; -a610 : IntPair; -ASSERT a610 = (6, 10); -ASSERT a610 IS_IN x; -a71 : IntPair; -ASSERT a71 = (7, 1); -ASSERT a71 IS_IN x; -a72 : IntPair; -ASSERT a72 = (7, 2); -ASSERT a72 IS_IN x; -a73 : IntPair; -ASSERT a73 = (7, 3); -ASSERT a73 IS_IN x; -a74 : IntPair; -ASSERT a74 = (7, 4); -ASSERT a74 IS_IN x; -a75 : IntPair; -ASSERT a75 = (7, 5); -ASSERT a75 IS_IN x; -a76 : IntPair; -ASSERT a76 = (7, 6); -ASSERT a76 IS_IN x; -a77 : IntPair; -ASSERT a77 = (7, 7); -ASSERT a77 IS_IN x; -a78 : IntPair; -ASSERT a78 = (7, 8); -ASSERT a78 IS_IN x; -a79 : IntPair; -ASSERT a79 = (7, 9); -ASSERT a79 IS_IN x; -a710 : IntPair; -ASSERT a710 = (7, 10); -ASSERT a710 IS_IN x; -a81 : IntPair; -ASSERT a81 = (8, 1); -ASSERT a81 IS_IN x; -a82 : IntPair; -ASSERT a82 = (8, 2); -ASSERT a82 IS_IN x; -a83 : IntPair; -ASSERT a83 = (8, 3); -ASSERT a83 IS_IN x; -a84 : IntPair; -ASSERT a84 = (8, 4); -ASSERT a84 IS_IN x; -a85 : IntPair; -ASSERT a85 = (8, 5); -ASSERT a85 IS_IN x; -a86 : IntPair; -ASSERT a86 = (8, 6); -ASSERT a86 IS_IN x; -a87 : IntPair; -ASSERT a87 = (8, 7); -ASSERT a87 IS_IN x; -a88 : IntPair; -ASSERT a88 = (8, 8); -ASSERT a88 IS_IN x; -a89 : IntPair; -ASSERT a89 = (8, 9); -ASSERT a89 IS_IN x; -a810 : IntPair; -ASSERT a810 = (8, 10); -ASSERT a810 IS_IN x; -a91 : IntPair; -ASSERT a91 = (9, 1); -ASSERT a91 IS_IN x; -a92 : IntPair; -ASSERT a92 = (9, 2); -ASSERT a92 IS_IN x; -a93 : IntPair; -ASSERT a93 = (9, 3); -ASSERT a93 IS_IN x; -a94 : IntPair; -ASSERT a94 = (9, 4); -ASSERT a94 IS_IN x; -a95 : IntPair; -ASSERT a95 = (9, 5); -ASSERT a95 IS_IN x; -a96 : IntPair; -ASSERT a96 = (9, 6); -ASSERT a96 IS_IN x; -a97 : IntPair; -ASSERT a97 = (9, 7); -ASSERT a97 IS_IN x; -a98 : IntPair; -ASSERT a98 = (9, 8); -ASSERT a98 IS_IN x; -a99 : IntPair; -ASSERT a99 = (9, 9); -ASSERT a99 IS_IN x; -a910 : IntPair; -ASSERT a910 = (9, 10); -ASSERT a910 IS_IN x; -a101 : IntPair; -ASSERT a101 = (10, 1); -ASSERT a101 IS_IN x; -a102 : IntPair; -ASSERT a102 = (10, 2); -ASSERT a102 IS_IN x; -a103 : IntPair; -ASSERT a103 = (10, 3); -ASSERT a103 IS_IN x; -a104 : IntPair; -ASSERT a104 = (10, 4); -ASSERT a104 IS_IN x; -a105 : IntPair; -ASSERT a105 = (10, 5); -ASSERT a105 IS_IN x; -a106 : IntPair; -ASSERT a106 = (10, 6); -ASSERT a106 IS_IN x; -a107 : IntPair; -ASSERT a107 = (10, 7); -ASSERT a107 IS_IN x; -a108 : IntPair; -ASSERT a108 = (10, 8); -ASSERT a108 IS_IN x; -a109 : IntPair; -ASSERT a109 = (10, 9); -ASSERT a109 IS_IN x; -a1010 : IntPair; -ASSERT a1010 = (10, 10); -ASSERT a1010 IS_IN x; -b11 : IntPair; -ASSERT b11 = (1, 1); -ASSERT b11 IS_IN y; -b12 : IntPair; -ASSERT b12 = (1, 2); -ASSERT b12 IS_IN y; -b13 : IntPair; -ASSERT b13 = (1, 3); -ASSERT b13 IS_IN y; -b14 : IntPair; -ASSERT b14 = (1, 4); -ASSERT b14 IS_IN y; -b15 : IntPair; -ASSERT b15 = (1, 5); -ASSERT b15 IS_IN y; -b16 : IntPair; -ASSERT b16 = (1, 6); -ASSERT b16 IS_IN y; -b17 : IntPair; -ASSERT b17 = (1, 7); -ASSERT b17 IS_IN y; -b18 : IntPair; -ASSERT b18 = (1, 8); -ASSERT b18 IS_IN y; -b19 : IntPair; -ASSERT b19 = (1, 9); -ASSERT b19 IS_IN y; -b110 : IntPair; -ASSERT b110 = (1, 10); -ASSERT b110 IS_IN y; -b21 : IntPair; -ASSERT b21 = (2, 1); -ASSERT b21 IS_IN y; -b22 : IntPair; -ASSERT b22 = (2, 2); -ASSERT b22 IS_IN y; -b23 : IntPair; -ASSERT b23 = (2, 3); -ASSERT b23 IS_IN y; -b24 : IntPair; -ASSERT b24 = (2, 4); -ASSERT b24 IS_IN y; -b25 : IntPair; -ASSERT b25 = (2, 5); -ASSERT b25 IS_IN y; -b26 : IntPair; -ASSERT b26 = (2, 6); -ASSERT b26 IS_IN y; -b27 : IntPair; -ASSERT b27 = (2, 7); -ASSERT b27 IS_IN y; -b28 : IntPair; -ASSERT b28 = (2, 8); -ASSERT b28 IS_IN y; -b29 : IntPair; -ASSERT b29 = (2, 9); -ASSERT b29 IS_IN y; -b210 : IntPair; -ASSERT b210 = (2, 10); -ASSERT b210 IS_IN y; -b31 : IntPair; -ASSERT b31 = (3, 1); -ASSERT b31 IS_IN y; -b32 : IntPair; -ASSERT b32 = (3, 2); -ASSERT b32 IS_IN y; -b33 : IntPair; -ASSERT b33 = (3, 3); -ASSERT b33 IS_IN y; -b34 : IntPair; -ASSERT b34 = (3, 4); -ASSERT b34 IS_IN y; -b35 : IntPair; -ASSERT b35 = (3, 5); -ASSERT b35 IS_IN y; -b36 : IntPair; -ASSERT b36 = (3, 6); -ASSERT b36 IS_IN y; -b37 : IntPair; -ASSERT b37 = (3, 7); -ASSERT b37 IS_IN y; -b38 : IntPair; -ASSERT b38 = (3, 8); -ASSERT b38 IS_IN y; -b39 : IntPair; -ASSERT b39 = (3, 9); -ASSERT b39 IS_IN y; -b310 : IntPair; -ASSERT b310 = (3, 10); -ASSERT b310 IS_IN y; -b41 : IntPair; -ASSERT b41 = (4, 1); -ASSERT b41 IS_IN y; -b42 : IntPair; -ASSERT b42 = (4, 2); -ASSERT b42 IS_IN y; -b43 : IntPair; -ASSERT b43 = (4, 3); -ASSERT b43 IS_IN y; -b44 : IntPair; -ASSERT b44 = (4, 4); -ASSERT b44 IS_IN y; -b45 : IntPair; -ASSERT b45 = (4, 5); -ASSERT b45 IS_IN y; -b46 : IntPair; -ASSERT b46 = (4, 6); -ASSERT b46 IS_IN y; -b47 : IntPair; -ASSERT b47 = (4, 7); -ASSERT b47 IS_IN y; -b48 : IntPair; -ASSERT b48 = (4, 8); -ASSERT b48 IS_IN y; -b49 : IntPair; -ASSERT b49 = (4, 9); -ASSERT b49 IS_IN y; -b410 : IntPair; -ASSERT b410 = (4, 10); -ASSERT b410 IS_IN y; -b51 : IntPair; -ASSERT b51 = (5, 1); -ASSERT b51 IS_IN y; -b52 : IntPair; -ASSERT b52 = (5, 2); -ASSERT b52 IS_IN y; -b53 : IntPair; -ASSERT b53 = (5, 3); -ASSERT b53 IS_IN y; -b54 : IntPair; -ASSERT b54 = (5, 4); -ASSERT b54 IS_IN y; -b55 : IntPair; -ASSERT b55 = (5, 5); -ASSERT b55 IS_IN y; -b56 : IntPair; -ASSERT b56 = (5, 6); -ASSERT b56 IS_IN y; -b57 : IntPair; -ASSERT b57 = (5, 7); -ASSERT b57 IS_IN y; -b58 : IntPair; -ASSERT b58 = (5, 8); -ASSERT b58 IS_IN y; -b59 : IntPair; -ASSERT b59 = (5, 9); -ASSERT b59 IS_IN y; -b510 : IntPair; -ASSERT b510 = (5, 10); -ASSERT b510 IS_IN y; -b61 : IntPair; -ASSERT b61 = (6, 1); -ASSERT b61 IS_IN y; -b62 : IntPair; -ASSERT b62 = (6, 2); -ASSERT b62 IS_IN y; -b63 : IntPair; -ASSERT b63 = (6, 3); -ASSERT b63 IS_IN y; -b64 : IntPair; -ASSERT b64 = (6, 4); -ASSERT b64 IS_IN y; -b65 : IntPair; -ASSERT b65 = (6, 5); -ASSERT b65 IS_IN y; -b66 : IntPair; -ASSERT b66 = (6, 6); -ASSERT b66 IS_IN y; -b67 : IntPair; -ASSERT b67 = (6, 7); -ASSERT b67 IS_IN y; -b68 : IntPair; -ASSERT b68 = (6, 8); -ASSERT b68 IS_IN y; -b69 : IntPair; -ASSERT b69 = (6, 9); -ASSERT b69 IS_IN y; -b610 : IntPair; -ASSERT b610 = (6, 10); -ASSERT b610 IS_IN y; -b71 : IntPair; -ASSERT b71 = (7, 1); -ASSERT b71 IS_IN y; -b72 : IntPair; -ASSERT b72 = (7, 2); -ASSERT b72 IS_IN y; -b73 : IntPair; -ASSERT b73 = (7, 3); -ASSERT b73 IS_IN y; -b74 : IntPair; -ASSERT b74 = (7, 4); -ASSERT b74 IS_IN y; -b75 : IntPair; -ASSERT b75 = (7, 5); -ASSERT b75 IS_IN y; -b76 : IntPair; -ASSERT b76 = (7, 6); -ASSERT b76 IS_IN y; -b77 : IntPair; -ASSERT b77 = (7, 7); -ASSERT b77 IS_IN y; -b78 : IntPair; -ASSERT b78 = (7, 8); -ASSERT b78 IS_IN y; -b79 : IntPair; -ASSERT b79 = (7, 9); -ASSERT b79 IS_IN y; -b710 : IntPair; -ASSERT b710 = (7, 10); -ASSERT b710 IS_IN y; -b81 : IntPair; -ASSERT b81 = (8, 1); -ASSERT b81 IS_IN y; -b82 : IntPair; -ASSERT b82 = (8, 2); -ASSERT b82 IS_IN y; -b83 : IntPair; -ASSERT b83 = (8, 3); -ASSERT b83 IS_IN y; -b84 : IntPair; -ASSERT b84 = (8, 4); -ASSERT b84 IS_IN y; -b85 : IntPair; -ASSERT b85 = (8, 5); -ASSERT b85 IS_IN y; -b86 : IntPair; -ASSERT b86 = (8, 6); -ASSERT b86 IS_IN y; -b87 : IntPair; -ASSERT b87 = (8, 7); -ASSERT b87 IS_IN y; -b88 : IntPair; -ASSERT b88 = (8, 8); -ASSERT b88 IS_IN y; -b89 : IntPair; -ASSERT b89 = (8, 9); -ASSERT b89 IS_IN y; -b810 : IntPair; -ASSERT b810 = (8, 10); -ASSERT b810 IS_IN y; -b91 : IntPair; -ASSERT b91 = (9, 1); -ASSERT b91 IS_IN y; -b92 : IntPair; -ASSERT b92 = (9, 2); -ASSERT b92 IS_IN y; -b93 : IntPair; -ASSERT b93 = (9, 3); -ASSERT b93 IS_IN y; -b94 : IntPair; -ASSERT b94 = (9, 4); -ASSERT b94 IS_IN y; -b95 : IntPair; -ASSERT b95 = (9, 5); -ASSERT b95 IS_IN y; -b96 : IntPair; -ASSERT b96 = (9, 6); -ASSERT b96 IS_IN y; -b97 : IntPair; -ASSERT b97 = (9, 7); -ASSERT b97 IS_IN y; -b98 : IntPair; -ASSERT b98 = (9, 8); -ASSERT b98 IS_IN y; -b99 : IntPair; -ASSERT b99 = (9, 9); -ASSERT b99 IS_IN y; -b910 : IntPair; -ASSERT b910 = (9, 10); -ASSERT b910 IS_IN y; -b101 : IntPair; -ASSERT b101 = (10, 1); -ASSERT b101 IS_IN y; -b102 : IntPair; -ASSERT b102 = (10, 2); -ASSERT b102 IS_IN y; -b103 : IntPair; -ASSERT b103 = (10, 3); -ASSERT b103 IS_IN y; -b104 : IntPair; -ASSERT b104 = (10, 4); -ASSERT b104 IS_IN y; -b105 : IntPair; -ASSERT b105 = (10, 5); -ASSERT b105 IS_IN y; -b106 : IntPair; -ASSERT b106 = (10, 6); -ASSERT b106 IS_IN y; -b107 : IntPair; -ASSERT b107 = (10, 7); -ASSERT b107 IS_IN y; -b108 : IntPair; -ASSERT b108 = (10, 8); -ASSERT b108 IS_IN y; -b109 : IntPair; -ASSERT b109 = (10, 9); -ASSERT b109 IS_IN y; -b1010 : IntPair; -ASSERT b1010 = (10, 10); -ASSERT b1010 IS_IN y; - -ASSERT (1, 9) IS_IN z; - -a : IntPair; -ASSERT a = (9,1); -ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); -ASSERT NOT (a IS_IN (TRANSPOSE r)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0.cvc b/test/regress/regress0/sets/rels/rel_product_0.cvc deleted file mode 100644 index 09981be0b..000000000 --- a/test/regress/regress0/sets/rels/rel_product_0.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT, INT, 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 : IntTup; -ASSERT v = (1,2,2,1); - -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT NOT (v IS_IN (x PRODUCT y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_0_1.cvc b/test/regress/regress0/sets/rels/rel_product_0_1.cvc deleted file mode 100644 index f141c7bd4..000000000 --- a/test/regress/regress0/sets/rels/rel_product_0_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT, INT, 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 : IntTup; -ASSERT v = (1,2,2,1); - -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT v IS_IN (x PRODUCT y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_product_1.cvc b/test/regress/regress0/sets/rels/rel_product_1.cvc deleted file mode 100644 index 1826e5a75..000000000 --- a/test/regress/regress0/sets/rels/rel_product_1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -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; - -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 NOT (v IS_IN (x PRODUCT 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 deleted file mode 100644 index 9559b74e1..000000000 --- a/test/regress/regress0/sets/rels/rel_product_1_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: SAT -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT, INT]; -IntTup: TYPE = [INT, INT, INT, INT,INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntTup; - -z : IntPair; -ASSERT z = (1,2,3); -zt : IntPair; -ASSERT zt = (3,2,1); - - -ASSERT z IS_IN x; -ASSERT zt IS_IN 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_symbolic_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc deleted file mode 100644 index 08ed32411..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; -f : INT; -d : IntPair; -ASSERT d = (f,3); -ASSERT d IS_IN y; -e : IntPair; -ASSERT e = (4, f); -ASSERT e IS_IN x; - -a : IntPair; -ASSERT a = (4,3); - -ASSERT r = (x JOIN y); - -ASSERT NOT (a IS_IN r); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc deleted file mode 100644 index df2d7f412..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_1_1.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; -r : SET OF IntPair; - -d : IntPair; -ASSERT d IS_IN y; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); - -ASSERT r = (x JOIN y); - -ASSERT NOT (e IS_IN r); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc deleted file mode 100644 index 082604dc2..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_2_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -d : IntPair; -ASSERT d = (1,3); -ASSERT (1,3) IS_IN y; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); - -ASSERT r = (x JOIN y); - -ASSERT NOT (e IS_IN r); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc deleted file mode 100644 index b1720b50e..000000000 --- a/test/regress/regress0/sets/rels/rel_symbolic_3_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; -f : INT; -d : IntPair; -ASSERT d IS_IN y; - -e : IntPair; -ASSERT e = (4, f); -ASSERT e IS_IN x; - -a : IntPair; -ASSERT a = (4,3); - -ASSERT r = (x JOIN y); - -ASSERT NOT (a IS_IN r); -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 deleted file mode 100644 index 67c444070..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_10_1.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 deleted file mode 100644 index 7edeb0efb..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_11.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 deleted file mode 100644 index d5d42eaad..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_2_1.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% 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 deleted file mode 100644 index 39564c4cf..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_3.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 (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 deleted file mode 100644 index e48ba4eb6..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_3_1.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 deleted file mode 100644 index decd38fe1..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_4.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 deleted file mode 100644 index 8ee75f7e9..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_4_1.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 deleted file mode 100644 index fd9caeade..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_5_1.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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 deleted file mode 100644 index 4570c5a8d..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_6.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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 deleted file mode 100644 index 15c0510a6..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_7.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 deleted file mode 100644 index 9f5879c6d..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_8.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 deleted file mode 100644 index f884349b1..000000000 --- a/test/regress/regress0/sets/rels/rel_tc_9_1.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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_tp_2.cvc b/test/regress/regress0/sets/rels/rel_tp_2.cvc deleted file mode 100644 index 441e79c45..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_2.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -ASSERT (z = TRANSPOSE(y) OR z = TRANSPOSE(x)); -ASSERT NOT (TRANSPOSE(z) = y); -ASSERT NOT (TRANSPOSE(z) = x); -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_0.cvc deleted file mode 100644 index a03f0e3fd..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_0.cvc +++ /dev/null @@ -1,32 +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 = (5,1); - -b : IntPair; -ASSERT b = (7, 5); - -ASSERT (1, 7) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (3, 4) IS_IN x; - -ASSERT b IS_IN y; -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT r = (x JOIN y); -ASSERT z IS_IN x; -ASSERT zt IS_IN y; -ASSERT NOT (a IS_IN (TRANSPOSE r)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc deleted file mode 100644 index 60b6edf58..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% 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; - -b : IntPair; -ASSERT b = (1,7); -c : IntPair; -ASSERT c = (2,3); -ASSERT b IS_IN x; -ASSERT c IS_IN x; - -d : IntPair; -ASSERT d = (7,3); -e : IntPair; -ASSERT e = (4,7); - -ASSERT d IS_IN y; -ASSERT e IS_IN y; - -ASSERT (3, 4) IS_IN z; - -a : IntPair; -ASSERT a = (4,1); - -ASSERT r = ((x JOIN y) JOIN z); - -ASSERT NOT (a IS_IN (TRANSPOSE r)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2.cvc deleted file mode 100644 index cc851f622..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_2.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; - -ASSERT (7, 1) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT (3, 4) IS_IN z; - -a : IntPair; -ASSERT a = (4,1); -ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); -ASSERT NOT (a IS_IN (TRANSPOSE r)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc deleted file mode 100644 index 04856d825..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_2_1.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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; -ASSERT (7, 1) IS_IN x; -ASSERT (2, 3) IS_IN x; - -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT (3, 4) IS_IN z; -a : IntPair; -ASSERT a = (4,1); - -ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z); -ASSERT a IS_IN (TRANSPOSE r); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc b/test/regress/regress0/sets/rels/rel_tp_join_3.cvc deleted file mode 100644 index 25277f43a..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_3.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% EXPECT: unsat -% crash on this -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -r : SET OF IntPair; - -ASSERT (7, 1) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT (3, 4) IS_IN z; -ASSERT (3, 3) IS_IN w; - -a : IntPair; -ASSERT a = (4,1); -%ASSERT r = (((TRANSPOSE x) JOIN y) JOIN (w JOIN z)); -ASSERT NOT (a IS_IN (TRANSPOSE r)); - -zz : SET OF IntPair; -ASSERT zz = ((TRANSPOSE x) JOIN y); -ASSERT NOT ((1,3) IS_IN w); -ASSERT NOT ((1,3) IS_IN (w | zz) ); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc deleted file mode 100644 index 54e16dd51..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% 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; - - -ASSERT x = {(1,7), (2,3)}; - -d : IntPair; -ASSERT d = (7,3); -e : IntPair; -ASSERT e = (4,7); - -ASSERT d IS_IN y; -ASSERT e IS_IN y; - -ASSERT (3, 4) IS_IN z; - -a : IntPair; -ASSERT a = (4,1); - -ASSERT r = ((x JOIN y) JOIN z); - -ASSERT NOT (a IS_IN (TRANSPOSE r)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc deleted file mode 100644 index 8d149a48d..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_int.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: unsat -% crash on this -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -r : SET OF IntPair; - -t : INT; -u : INT; - -ASSERT 4 < t AND t < 6; -ASSERT 4 < u AND u < 6; - -ASSERT (1, u) IS_IN x; -ASSERT (t, 3) IS_IN y; - -a : IntPair; -ASSERT a = (1,3); - -ASSERT NOT (a IS_IN (x JOIN y)); - - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc deleted file mode 100644 index b05026bc9..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_pro_0.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 IntPair; -r : SET OF IntTup; - -ASSERT (2, 1) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (2, 2) IS_IN y; -ASSERT (4, 7) IS_IN y; -ASSERT (3, 4) IS_IN z; - -v : IntTup; -ASSERT v = (4,3,2,1); - -ASSERT r = (((TRANSPOSE x) JOIN y) PRODUCT z); -ASSERT NOT (v IS_IN (TRANSPOSE r)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc deleted file mode 100644 index aacf6c054..000000000 --- a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -r : SET OF IntPair; - -t : INT; -u : INT; - -ASSERT 4 < t AND t < 6; -ASSERT 4 < u AND u < 6; - -ASSERT (1, t) IS_IN x; -ASSERT (u, 3) IS_IN y; - -a : IntPair; -ASSERT a = (1,3); - -ASSERT NOT (a IS_IN (x JOIN y)); - -st : SET OF INT; -su : SET OF INT; -ASSERT t IS_IN st; -ASSERT u IS_IN su; -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_0.cvc b/test/regress/regress0/sets/rels/rel_transpose_0.cvc deleted file mode 100644 index 49fb87569..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_0.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -a: INT; -z : IntPair; -ASSERT z = (1,2); -zt : IntPair; -ASSERT zt = (2,1); - -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE x)); - -ASSERT y = (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 deleted file mode 100644 index bdcf31bb8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_1.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 deleted file mode 100644 index fa6ee5069..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_1_1.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT, INT, INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z : IntTup; -a: INT; -ASSERT z = (1,2,a); -zt : IntTup; -ASSERT zt = (3,2,2); -ASSERT z IS_IN x; -ASSERT zt IS_IN (TRANSPOSE x); -ASSERT y = (TRANSPOSE x); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_3.cvc b/test/regress/regress0/sets/rels/rel_transpose_3.cvc deleted file mode 100644 index 225f3491c..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_3.cvc +++ /dev/null @@ -1,14 +0,0 @@ -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 (x = y); -ASSERT z IS_IN x; -ASSERT NOT (zt IS_IN (TRANSPOSE y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_4.cvc b/test/regress/regress0/sets/rels/rel_transpose_4.cvc deleted file mode 100644 index b260147c8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_4.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -z : IntPair; -ASSERT z = (1,2); - -ASSERT z IS_IN x; -ASSERT NOT ((2, 1) IS_IN (TRANSPOSE x)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_5.cvc b/test/regress/regress0/sets/rels/rel_transpose_5.cvc deleted file mode 100644 index 203e8b3d2..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_5.cvc +++ /dev/null @@ -1,22 +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); -ASSERT zt IS_IN y; - -w : IntPair; -ASSERT w = (2, 2); -ASSERT w IS_IN y; -ASSERT z IS_IN x; - -ASSERT NOT (zt IS_IN (TRANSPOSE (x JOIN y))); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_6.cvc b/test/regress/regress0/sets/rels/rel_transpose_6.cvc deleted file mode 100644 index a2e8bcf10..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_6.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% 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 (3, 4) IS_IN x; -ASSERT (3, 5) IS_IN x; -ASSERT (3, 3) IS_IN x; - -ASSERT x = TRANSPOSE(y); - -ASSERT NOT (zt IS_IN y); - -ASSERT z IS_IN y; -ASSERT NOT (zt IS_IN (TRANSPOSE y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/rel_transpose_7.cvc b/test/regress/regress0/sets/rels/rel_transpose_7.cvc deleted file mode 100644 index bcc3babc8..000000000 --- a/test/regress/regress0/sets/rels/rel_transpose_7.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -ASSERT x = y; -ASSERT NOT (TRANSPOSE(x) = TRANSPOSE(y)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc b/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc deleted file mode 100644 index dd5995c42..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/garbage_collect.cvc +++ /dev/null @@ -1,59 +0,0 @@ -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/tobesolved/rel_1tup_syntax.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc deleted file mode 100644 index 0b4a13d09..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_1tup_syntax.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntTup: TYPE = [INT]; -IntPair: TYPE = [INT, INT]; -x : SET OF IntTup; -y : SET OF IntTup; -z: SET OF IntTup; - -b : IntTup; -ASSERT b = TUPLE(2); -ASSERT b IS_IN x; - -a : IntTup; -ASSERT a = TUPLE(1); -ASSERT a IS_IN y; - -c : IntTup; -ASSERT c = TUPLE(2); - -ASSERT z = (x JOIN y); - -ASSERT NOT (c IS_IN z); - -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc deleted file mode 100644 index 5dfe957ca..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_complex_2.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% 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; - - -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 = (4,3); -ASSERT h IS_IN x; -ASSERT h IS_IN y; - -ASSERT r = (x JOIN y); - -e : IntPair; - -ASSERT r = (x | y); -ASSERT NOT(z = (x & y)); -ASSERT z = (x - y); -ASSERT x <= y; -ASSERT e IS_IN (z JOIN x); -ASSERT e IS_IN x; -ASSERT e IS_IN (x & y); -CHECKSAT TRUE;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc deleted file mode 100644 index 60e39a5b2..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_complex_4.cvc +++ /dev/null @@ -1,652 +0,0 @@ -% 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; - -a11 : IntPair; -ASSERT a11 = (1, 1); -ASSERT a11 IS_IN x; -a12 : IntPair; -ASSERT a12 = (1, 2); -ASSERT a12 IS_IN x; -a13 : IntPair; -ASSERT a13 = (1, 3); -ASSERT a13 IS_IN x; -a14 : IntPair; -ASSERT a14 = (1, 4); -ASSERT a14 IS_IN x; -a15 : IntPair; -ASSERT a15 = (1, 5); -ASSERT a15 IS_IN x; -a16 : IntPair; -ASSERT a16 = (1, 6); -ASSERT a16 IS_IN x; -a17 : IntPair; -ASSERT a17 = (1, 7); -ASSERT a17 IS_IN x; -a18 : IntPair; -ASSERT a18 = (1, 8); -ASSERT a18 IS_IN x; -a19 : IntPair; -ASSERT a19 = (1, 9); -ASSERT a19 IS_IN x; -a110 : IntPair; -ASSERT a110 = (1, 10); -ASSERT a110 IS_IN x; -a21 : IntPair; -ASSERT a21 = (2, 1); -ASSERT a21 IS_IN x; -a22 : IntPair; -ASSERT a22 = (2, 2); -ASSERT a22 IS_IN x; -a23 : IntPair; -ASSERT a23 = (2, 3); -ASSERT a23 IS_IN x; -a24 : IntPair; -ASSERT a24 = (2, 4); -ASSERT a24 IS_IN x; -a25 : IntPair; -ASSERT a25 = (2, 5); -ASSERT a25 IS_IN x; -a26 : IntPair; -ASSERT a26 = (2, 6); -ASSERT a26 IS_IN x; -a27 : IntPair; -ASSERT a27 = (2, 7); -ASSERT a27 IS_IN x; -a28 : IntPair; -ASSERT a28 = (2, 8); -ASSERT a28 IS_IN x; -a29 : IntPair; -ASSERT a29 = (2, 9); -ASSERT a29 IS_IN x; -a210 : IntPair; -ASSERT a210 = (2, 10); -ASSERT a210 IS_IN x; -a31 : IntPair; -ASSERT a31 = (3, 1); -ASSERT a31 IS_IN x; -a32 : IntPair; -ASSERT a32 = (3, 2); -ASSERT a32 IS_IN x; -a33 : IntPair; -ASSERT a33 = (3, 3); -ASSERT a33 IS_IN x; -a34 : IntPair; -ASSERT a34 = (3, 4); -ASSERT a34 IS_IN x; -a35 : IntPair; -ASSERT a35 = (3, 5); -ASSERT a35 IS_IN x; -a36 : IntPair; -ASSERT a36 = (3, 6); -ASSERT a36 IS_IN x; -a37 : IntPair; -ASSERT a37 = (3, 7); -ASSERT a37 IS_IN x; -a38 : IntPair; -ASSERT a38 = (3, 8); -ASSERT a38 IS_IN x; -a39 : IntPair; -ASSERT a39 = (3, 9); -ASSERT a39 IS_IN x; -a310 : IntPair; -ASSERT a310 = (3, 10); -ASSERT a310 IS_IN x; -a41 : IntPair; -ASSERT a41 = (4, 1); -ASSERT a41 IS_IN x; -a42 : IntPair; -ASSERT a42 = (4, 2); -ASSERT a42 IS_IN x; -a43 : IntPair; -ASSERT a43 = (4, 3); -ASSERT a43 IS_IN x; -a44 : IntPair; -ASSERT a44 = (4, 4); -ASSERT a44 IS_IN x; -a45 : IntPair; -ASSERT a45 = (4, 5); -ASSERT a45 IS_IN x; -a46 : IntPair; -ASSERT a46 = (4, 6); -ASSERT a46 IS_IN x; -a47 : IntPair; -ASSERT a47 = (4, 7); -ASSERT a47 IS_IN x; -a48 : IntPair; -ASSERT a48 = (4, 8); -ASSERT a48 IS_IN x; -a49 : IntPair; -ASSERT a49 = (4, 9); -ASSERT a49 IS_IN x; -a410 : IntPair; -ASSERT a410 = (4, 10); -ASSERT a410 IS_IN x; -a51 : IntPair; -ASSERT a51 = (5, 1); -ASSERT a51 IS_IN x; -a52 : IntPair; -ASSERT a52 = (5, 2); -ASSERT a52 IS_IN x; -a53 : IntPair; -ASSERT a53 = (5, 3); -ASSERT a53 IS_IN x; -a54 : IntPair; -ASSERT a54 = (5, 4); -ASSERT a54 IS_IN x; -a55 : IntPair; -ASSERT a55 = (5, 5); -ASSERT a55 IS_IN x; -a56 : IntPair; -ASSERT a56 = (5, 6); -ASSERT a56 IS_IN x; -a57 : IntPair; -ASSERT a57 = (5, 7); -ASSERT a57 IS_IN x; -a58 : IntPair; -ASSERT a58 = (5, 8); -ASSERT a58 IS_IN x; -a59 : IntPair; -ASSERT a59 = (5, 9); -ASSERT a59 IS_IN x; -a510 : IntPair; -ASSERT a510 = (5, 10); -ASSERT a510 IS_IN x; -a61 : IntPair; -ASSERT a61 = (6, 1); -ASSERT a61 IS_IN x; -a62 : IntPair; -ASSERT a62 = (6, 2); -ASSERT a62 IS_IN x; -a63 : IntPair; -ASSERT a63 = (6, 3); -ASSERT a63 IS_IN x; -a64 : IntPair; -ASSERT a64 = (6, 4); -ASSERT a64 IS_IN x; -a65 : IntPair; -ASSERT a65 = (6, 5); -ASSERT a65 IS_IN x; -a66 : IntPair; -ASSERT a66 = (6, 6); -ASSERT a66 IS_IN x; -a67 : IntPair; -ASSERT a67 = (6, 7); -ASSERT a67 IS_IN x; -a68 : IntPair; -ASSERT a68 = (6, 8); -ASSERT a68 IS_IN x; -a69 : IntPair; -ASSERT a69 = (6, 9); -ASSERT a69 IS_IN x; -a610 : IntPair; -ASSERT a610 = (6, 10); -ASSERT a610 IS_IN x; -a71 : IntPair; -ASSERT a71 = (7, 1); -ASSERT a71 IS_IN x; -a72 : IntPair; -ASSERT a72 = (7, 2); -ASSERT a72 IS_IN x; -a73 : IntPair; -ASSERT a73 = (7, 3); -ASSERT a73 IS_IN x; -a74 : IntPair; -ASSERT a74 = (7, 4); -ASSERT a74 IS_IN x; -a75 : IntPair; -ASSERT a75 = (7, 5); -ASSERT a75 IS_IN x; -a76 : IntPair; -ASSERT a76 = (7, 6); -ASSERT a76 IS_IN x; -a77 : IntPair; -ASSERT a77 = (7, 7); -ASSERT a77 IS_IN x; -a78 : IntPair; -ASSERT a78 = (7, 8); -ASSERT a78 IS_IN x; -a79 : IntPair; -ASSERT a79 = (7, 9); -ASSERT a79 IS_IN x; -a710 : IntPair; -ASSERT a710 = (7, 10); -ASSERT a710 IS_IN x; -a81 : IntPair; -ASSERT a81 = (8, 1); -ASSERT a81 IS_IN x; -a82 : IntPair; -ASSERT a82 = (8, 2); -ASSERT a82 IS_IN x; -a83 : IntPair; -ASSERT a83 = (8, 3); -ASSERT a83 IS_IN x; -a84 : IntPair; -ASSERT a84 = (8, 4); -ASSERT a84 IS_IN x; -a85 : IntPair; -ASSERT a85 = (8, 5); -ASSERT a85 IS_IN x; -a86 : IntPair; -ASSERT a86 = (8, 6); -ASSERT a86 IS_IN x; -a87 : IntPair; -ASSERT a87 = (8, 7); -ASSERT a87 IS_IN x; -a88 : IntPair; -ASSERT a88 = (8, 8); -ASSERT a88 IS_IN x; -a89 : IntPair; -ASSERT a89 = (8, 9); -ASSERT a89 IS_IN x; -a810 : IntPair; -ASSERT a810 = (8, 10); -ASSERT a810 IS_IN x; -a91 : IntPair; -ASSERT a91 = (9, 1); -ASSERT a91 IS_IN x; -a92 : IntPair; -ASSERT a92 = (9, 2); -ASSERT a92 IS_IN x; -a93 : IntPair; -ASSERT a93 = (9, 3); -ASSERT a93 IS_IN x; -a94 : IntPair; -ASSERT a94 = (9, 4); -ASSERT a94 IS_IN x; -a95 : IntPair; -ASSERT a95 = (9, 5); -ASSERT a95 IS_IN x; -a96 : IntPair; -ASSERT a96 = (9, 6); -ASSERT a96 IS_IN x; -a97 : IntPair; -ASSERT a97 = (9, 7); -ASSERT a97 IS_IN x; -a98 : IntPair; -ASSERT a98 = (9, 8); -ASSERT a98 IS_IN x; -a99 : IntPair; -ASSERT a99 = (9, 9); -ASSERT a99 IS_IN x; -a910 : IntPair; -ASSERT a910 = (9, 10); -ASSERT a910 IS_IN x; -a101 : IntPair; -ASSERT a101 = (10, 1); -ASSERT a101 IS_IN x; -a102 : IntPair; -ASSERT a102 = (10, 2); -ASSERT a102 IS_IN x; -a103 : IntPair; -ASSERT a103 = (10, 3); -ASSERT a103 IS_IN x; -a104 : IntPair; -ASSERT a104 = (10, 4); -ASSERT a104 IS_IN x; -a105 : IntPair; -ASSERT a105 = (10, 5); -ASSERT a105 IS_IN x; -a106 : IntPair; -ASSERT a106 = (10, 6); -ASSERT a106 IS_IN x; -a107 : IntPair; -ASSERT a107 = (10, 7); -ASSERT a107 IS_IN x; -a108 : IntPair; -ASSERT a108 = (10, 8); -ASSERT a108 IS_IN x; -a109 : IntPair; -ASSERT a109 = (10, 9); -ASSERT a109 IS_IN x; -a1010 : IntPair; -ASSERT a1010 = (10, 10); -ASSERT a1010 IS_IN x; -b11 : IntPair; -ASSERT b11 = (1, 1); -ASSERT b11 IS_IN y; -b12 : IntPair; -ASSERT b12 = (1, 2); -ASSERT b12 IS_IN y; -b13 : IntPair; -ASSERT b13 = (1, 3); -ASSERT b13 IS_IN y; -b14 : IntPair; -ASSERT b14 = (1, 4); -ASSERT b14 IS_IN y; -b15 : IntPair; -ASSERT b15 = (1, 5); -ASSERT b15 IS_IN y; -b16 : IntPair; -ASSERT b16 = (1, 6); -ASSERT b16 IS_IN y; -b17 : IntPair; -ASSERT b17 = (1, 7); -ASSERT b17 IS_IN y; -b18 : IntPair; -ASSERT b18 = (1, 8); -ASSERT b18 IS_IN y; -b19 : IntPair; -ASSERT b19 = (1, 9); -ASSERT b19 IS_IN y; -b110 : IntPair; -ASSERT b110 = (1, 10); -ASSERT b110 IS_IN y; -b21 : IntPair; -ASSERT b21 = (2, 1); -ASSERT b21 IS_IN y; -b22 : IntPair; -ASSERT b22 = (2, 2); -ASSERT b22 IS_IN y; -b23 : IntPair; -ASSERT b23 = (2, 3); -ASSERT b23 IS_IN y; -b24 : IntPair; -ASSERT b24 = (2, 4); -ASSERT b24 IS_IN y; -b25 : IntPair; -ASSERT b25 = (2, 5); -ASSERT b25 IS_IN y; -b26 : IntPair; -ASSERT b26 = (2, 6); -ASSERT b26 IS_IN y; -b27 : IntPair; -ASSERT b27 = (2, 7); -ASSERT b27 IS_IN y; -b28 : IntPair; -ASSERT b28 = (2, 8); -ASSERT b28 IS_IN y; -b29 : IntPair; -ASSERT b29 = (2, 9); -ASSERT b29 IS_IN y; -b210 : IntPair; -ASSERT b210 = (2, 10); -ASSERT b210 IS_IN y; -b31 : IntPair; -ASSERT b31 = (3, 1); -ASSERT b31 IS_IN y; -b32 : IntPair; -ASSERT b32 = (3, 2); -ASSERT b32 IS_IN y; -b33 : IntPair; -ASSERT b33 = (3, 3); -ASSERT b33 IS_IN y; -b34 : IntPair; -ASSERT b34 = (3, 4); -ASSERT b34 IS_IN y; -b35 : IntPair; -ASSERT b35 = (3, 5); -ASSERT b35 IS_IN y; -b36 : IntPair; -ASSERT b36 = (3, 6); -ASSERT b36 IS_IN y; -b37 : IntPair; -ASSERT b37 = (3, 7); -ASSERT b37 IS_IN y; -b38 : IntPair; -ASSERT b38 = (3, 8); -ASSERT b38 IS_IN y; -b39 : IntPair; -ASSERT b39 = (3, 9); -ASSERT b39 IS_IN y; -b310 : IntPair; -ASSERT b310 = (3, 10); -ASSERT b310 IS_IN y; -b41 : IntPair; -ASSERT b41 = (4, 1); -ASSERT b41 IS_IN y; -b42 : IntPair; -ASSERT b42 = (4, 2); -ASSERT b42 IS_IN y; -b43 : IntPair; -ASSERT b43 = (4, 3); -ASSERT b43 IS_IN y; -b44 : IntPair; -ASSERT b44 = (4, 4); -ASSERT b44 IS_IN y; -b45 : IntPair; -ASSERT b45 = (4, 5); -ASSERT b45 IS_IN y; -b46 : IntPair; -ASSERT b46 = (4, 6); -ASSERT b46 IS_IN y; -b47 : IntPair; -ASSERT b47 = (4, 7); -ASSERT b47 IS_IN y; -b48 : IntPair; -ASSERT b48 = (4, 8); -ASSERT b48 IS_IN y; -b49 : IntPair; -ASSERT b49 = (4, 9); -ASSERT b49 IS_IN y; -b410 : IntPair; -ASSERT b410 = (4, 10); -ASSERT b410 IS_IN y; -b51 : IntPair; -ASSERT b51 = (5, 1); -ASSERT b51 IS_IN y; -b52 : IntPair; -ASSERT b52 = (5, 2); -ASSERT b52 IS_IN y; -b53 : IntPair; -ASSERT b53 = (5, 3); -ASSERT b53 IS_IN y; -b54 : IntPair; -ASSERT b54 = (5, 4); -ASSERT b54 IS_IN y; -b55 : IntPair; -ASSERT b55 = (5, 5); -ASSERT b55 IS_IN y; -b56 : IntPair; -ASSERT b56 = (5, 6); -ASSERT b56 IS_IN y; -b57 : IntPair; -ASSERT b57 = (5, 7); -ASSERT b57 IS_IN y; -b58 : IntPair; -ASSERT b58 = (5, 8); -ASSERT b58 IS_IN y; -b59 : IntPair; -ASSERT b59 = (5, 9); -ASSERT b59 IS_IN y; -b510 : IntPair; -ASSERT b510 = (5, 10); -ASSERT b510 IS_IN y; -b61 : IntPair; -ASSERT b61 = (6, 1); -ASSERT b61 IS_IN y; -b62 : IntPair; -ASSERT b62 = (6, 2); -ASSERT b62 IS_IN y; -b63 : IntPair; -ASSERT b63 = (6, 3); -ASSERT b63 IS_IN y; -b64 : IntPair; -ASSERT b64 = (6, 4); -ASSERT b64 IS_IN y; -b65 : IntPair; -ASSERT b65 = (6, 5); -ASSERT b65 IS_IN y; -b66 : IntPair; -ASSERT b66 = (6, 6); -ASSERT b66 IS_IN y; -b67 : IntPair; -ASSERT b67 = (6, 7); -ASSERT b67 IS_IN y; -b68 : IntPair; -ASSERT b68 = (6, 8); -ASSERT b68 IS_IN y; -b69 : IntPair; -ASSERT b69 = (6, 9); -ASSERT b69 IS_IN y; -b610 : IntPair; -ASSERT b610 = (6, 10); -ASSERT b610 IS_IN y; -b71 : IntPair; -ASSERT b71 = (7, 1); -ASSERT b71 IS_IN y; -b72 : IntPair; -ASSERT b72 = (7, 2); -ASSERT b72 IS_IN y; -b73 : IntPair; -ASSERT b73 = (7, 3); -ASSERT b73 IS_IN y; -b74 : IntPair; -ASSERT b74 = (7, 4); -ASSERT b74 IS_IN y; -b75 : IntPair; -ASSERT b75 = (7, 5); -ASSERT b75 IS_IN y; -b76 : IntPair; -ASSERT b76 = (7, 6); -ASSERT b76 IS_IN y; -b77 : IntPair; -ASSERT b77 = (7, 7); -ASSERT b77 IS_IN y; -b78 : IntPair; -ASSERT b78 = (7, 8); -ASSERT b78 IS_IN y; -b79 : IntPair; -ASSERT b79 = (7, 9); -ASSERT b79 IS_IN y; -b710 : IntPair; -ASSERT b710 = (7, 10); -ASSERT b710 IS_IN y; -b81 : IntPair; -ASSERT b81 = (8, 1); -ASSERT b81 IS_IN y; -b82 : IntPair; -ASSERT b82 = (8, 2); -ASSERT b82 IS_IN y; -b83 : IntPair; -ASSERT b83 = (8, 3); -ASSERT b83 IS_IN y; -b84 : IntPair; -ASSERT b84 = (8, 4); -ASSERT b84 IS_IN y; -b85 : IntPair; -ASSERT b85 = (8, 5); -ASSERT b85 IS_IN y; -b86 : IntPair; -ASSERT b86 = (8, 6); -ASSERT b86 IS_IN y; -b87 : IntPair; -ASSERT b87 = (8, 7); -ASSERT b87 IS_IN y; -b88 : IntPair; -ASSERT b88 = (8, 8); -ASSERT b88 IS_IN y; -b89 : IntPair; -ASSERT b89 = (8, 9); -ASSERT b89 IS_IN y; -b810 : IntPair; -ASSERT b810 = (8, 10); -ASSERT b810 IS_IN y; -b91 : IntPair; -ASSERT b91 = (9, 1); -ASSERT b91 IS_IN y; -b92 : IntPair; -ASSERT b92 = (9, 2); -ASSERT b92 IS_IN y; -b93 : IntPair; -ASSERT b93 = (9, 3); -ASSERT b93 IS_IN y; -b94 : IntPair; -ASSERT b94 = (9, 4); -ASSERT b94 IS_IN y; -b95 : IntPair; -ASSERT b95 = (9, 5); -ASSERT b95 IS_IN y; -b96 : IntPair; -ASSERT b96 = (9, 6); -ASSERT b96 IS_IN y; -b97 : IntPair; -ASSERT b97 = (9, 7); -ASSERT b97 IS_IN y; -b98 : IntPair; -ASSERT b98 = (9, 8); -ASSERT b98 IS_IN y; -b99 : IntPair; -ASSERT b99 = (9, 9); -ASSERT b99 IS_IN y; -b910 : IntPair; -ASSERT b910 = (9, 10); -ASSERT b910 IS_IN y; -b101 : IntPair; -ASSERT b101 = (10, 1); -ASSERT b101 IS_IN y; -b102 : IntPair; -ASSERT b102 = (10, 2); -ASSERT b102 IS_IN y; -b103 : IntPair; -ASSERT b103 = (10, 3); -ASSERT b103 IS_IN y; -b104 : IntPair; -ASSERT b104 = (10, 4); -ASSERT b104 IS_IN y; -b105 : IntPair; -ASSERT b105 = (10, 5); -ASSERT b105 IS_IN y; -b106 : IntPair; -ASSERT b106 = (10, 6); -ASSERT b106 IS_IN y; -b107 : IntPair; -ASSERT b107 = (10, 7); -ASSERT b107 IS_IN y; -b108 : IntPair; -ASSERT b108 = (10, 8); -ASSERT b108 IS_IN y; -b109 : IntPair; -ASSERT b109 = (10, 9); -ASSERT b109 IS_IN y; -b1010 : IntPair; -ASSERT b1010 = (10, 10); -ASSERT b1010 IS_IN y; - -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/tobesolved/rel_join_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc deleted file mode 100644 index 034eebd22..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_0.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; - -ASSERT (1, 2) IS_IN x; -ASSERT (2, 3) IS_IN x; -ASSERT (3, 4) IS_IN z; - -ASSERT ((1, 1) IS_IN (x JOIN x)); - -%ASSERT y = (x JOIN x); - -ASSERT (NOT (1,4) IS_IN ((x JOIN x) JOIN z)); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc deleted file mode 100644 index 5fce37ef4..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_com.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -a: INT; -b: INT; - -ASSERT (1, b) IS_IN x; -ASSERT (a, 3) IS_IN y; - -ASSERT NOT ((1,3) IS_IN (x JOIN y)); -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc deleted file mode 100644 index ca6369087..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_0.cvc +++ /dev/null @@ -1,35 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; - -r : SET OF IntPair; -r2 : SET OF IntPair; - -d : IntPair; -ASSERT d = (3,1); -ASSERT (1,3) IS_IN y; -ASSERT d IS_IN y; - -ASSERT (3,1) IS_IN y; -ASSERT (4,1) IS_IN y; -ASSERT (1,3) IS_IN z; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); -ASSERT e IS_IN x; - -ASSERT r = (x JOIN y); -ASSERT r2 = (y JOIN z); -ASSERT (1,3) IS_IN r; -ASSERT r = r2; -ASSERT NOT (e IS_IN r); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc deleted file mode 100644 index 32d529df3..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_join_cyc_1.cvc +++ /dev/null @@ -1,31 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -w : SET OF IntPair; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; - -r : SET OF IntPair; -r2 : SET OF IntPair; - -d : IntPair; -ASSERT d = (3,1); -ASSERT (1,3) IS_IN y; -ASSERT d IS_IN y; - -ASSERT (3,1) IS_IN y; -ASSERT (4,1) IS_IN y; -ASSERT (1,3) IS_IN z; - -a : IntPair; -ASSERT a IS_IN x; - -e : IntPair; -ASSERT e = (4,3); -ASSERT e IS_IN x; - -ASSERT y = ((x JOIN y) JOIN z); - - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc deleted file mode 100644 index 7257d5a0d..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_pt_0.cvc +++ /dev/null @@ -1,25 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT, INT, INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; -w : SET OF IntTup; - -z : IntPair; -ASSERT z = (1,3); -zt : IntPair; -ASSERT zt = (2,1); -v : IntTup; -ASSERT v = (1,2,2,1); - -ASSERT zt IS_IN y; -ASSERT v IS_IN (x PRODUCT y); -ASSERT (4, 4, 5, 5) IS_IN w; -ASSERT z IS_IN x; - -ASSERT w = (x PRODUCT y); -ASSERT NOT (4,4) IS_IN x; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc deleted file mode 100644 index 0a2ec79be..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tc_0.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; - -a : IntPair; -ASSERT a = (1,2); -b : IntPair; -ASSERT b = (2,1); -c: IntPair; -ASSERT c = (1,1); -d : IntPair; -ASSERT d = (1,5); - -ASSERT a IS_IN x; -ASSERT b IS_IN x; -ASSERT c IS_IN x; -ASSERT d IS_IN x; -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 1) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc deleted file mode 100644 index b8ab773b1..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tc_1.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -e: INT; -a : IntPair; -ASSERT a = (1,e); -b : IntPair; -ASSERT b = (e,1); - - -ASSERT a IS_IN x; -ASSERT b IS_IN x; - -ASSERT y = (TCLOSURE x); -ASSERT NOT ((1, 1) IS_IN y); - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc deleted file mode 100644 index f074011ce..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tp_3.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z: SET OF IntPair; - -ASSERT (1, 3) IS_IN x; -ASSERT ((2,3) IS_IN z OR (2,1) IS_IN z); -ASSERT y = (TRANSPOSE x); -ASSERT NOT (1,2) IS_IN y; -ASSERT NOT (3,2) IS_IN y; -ASSERT x = z; -CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc b/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc deleted file mode 100644 index 183be8d9b..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/rel_tp_4.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 NOT (2,1) IS_IN x; - -CHECKSAT; diff --git a/test/regress/regress0/sets/rels/tobesolved/test.cvc b/test/regress/regress0/sets/rels/tobesolved/test.cvc deleted file mode 100644 index aa4e17eab..000000000 --- a/test/regress/regress0/sets/rels/tobesolved/test.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; -ASSERT (y JOIN x) = x; - -ASSERT (1,2) IS_IN x; - -CHECKSAT; |