diff options
Diffstat (limited to 'test/regress/regress1/rels')
70 files changed, 1382 insertions, 1552 deletions
diff --git a/test/regress/regress1/rels/addr_book_1.cvc b/test/regress/regress1/rels/addr_book_1.cvc deleted file mode 100644 index 8e7cdbd9d..000000000 --- a/test/regress/regress1/rels/addr_book_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/addr_book_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1.cvc.smt2 new file mode 100644 index 000000000..7a6ac7d5b --- /dev/null +++ b/test/regress/regress1/rels/addr_book_1.cvc.smt2 @@ -0,0 +1,38 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(declare-sort Atom 0) + + + +(declare-fun Target () (Set (Tuple Atom))) +(declare-fun Name () (Set (Tuple Atom))) +(declare-fun Addr () (Set (Tuple Atom))) +(declare-fun Book () (Set (Tuple Atom))) +(declare-fun names () (Set (Tuple Atom Atom))) +(declare-fun addr () (Set (Tuple Atom Atom Atom))) +(declare-fun b1 () Atom) +(declare-fun b1_tup () (Tuple Atom)) +(assert (= b1_tup (mkTuple b1))) +(assert (member b1_tup Book)) +(declare-fun b2 () Atom) +(declare-fun b2_tup () (Tuple Atom)) +(assert (= b2_tup (mkTuple b2))) +(assert (member b2_tup Book)) +(declare-fun b3 () Atom) +(declare-fun b3_tup () (Tuple Atom)) +(assert (= b3_tup (mkTuple b3))) +(assert (member b3_tup Book)) +(declare-fun m () Atom) +(declare-fun m_tup () (Tuple Atom)) +(assert (= m_tup (mkTuple m))) +(assert (member m_tup Name)) +(declare-fun t () Atom) +(declare-fun t_tup () (Tuple Atom)) +(assert (= t_tup (mkTuple t))) +(assert (member t_tup Target)) +(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) +(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t))))) +(assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr)))) +(check-sat) diff --git a/test/regress/regress1/rels/addr_book_1_1.cvc b/test/regress/regress1/rels/addr_book_1_1.cvc deleted file mode 100644 index c320d925f..000000000 --- a/test/regress/regress1/rels/addr_book_1_1.cvc +++ /dev/null @@ -1,45 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/addr_book_1_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 new file mode 100644 index 000000000..29eb2106d --- /dev/null +++ b/test/regress/regress1/rels/addr_book_1_1.cvc.smt2 @@ -0,0 +1,38 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) +(declare-sort Atom 0) + + + +(declare-fun Target () (Set (Tuple Atom))) +(declare-fun Name () (Set (Tuple Atom))) +(declare-fun Addr () (Set (Tuple Atom))) +(declare-fun Book () (Set (Tuple Atom))) +(declare-fun names () (Set (Tuple Atom Atom))) +(declare-fun addr () (Set (Tuple Atom Atom Atom))) +(declare-fun b1 () Atom) +(declare-fun b1_tup () (Tuple Atom)) +(assert (= b1_tup (mkTuple b1))) +(assert (member b1_tup Book)) +(declare-fun b2 () Atom) +(declare-fun b2_tup () (Tuple Atom)) +(assert (= b2_tup (mkTuple b2))) +(assert (member b2_tup Book)) +(declare-fun b3 () Atom) +(declare-fun b3_tup () (Tuple Atom)) +(assert (= b3_tup (mkTuple b3))) +(assert (member b3_tup Book)) +(declare-fun m () Atom) +(declare-fun m_tup () (Tuple Atom)) +(assert (= m_tup (mkTuple m))) +(assert (member m_tup Name)) +(declare-fun t () Atom) +(declare-fun t_tup () (Tuple Atom)) +(assert (= t_tup (mkTuple t))) +(assert (member t_tup Target)) +(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) +(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr))) +(check-sat) diff --git a/test/regress/regress1/rels/bv1-unit.cvc b/test/regress/regress1/rels/bv1-unit.cvc deleted file mode 100644 index 95fb5f02c..000000000 --- a/test/regress/regress1/rels/bv1-unit.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -DATATYPE unit = u END; -BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BITVECTOR(1); -b : BITVECTOR(1); -c : BITVECTOR(1); -d : BITVECTOR(1); -e : BITVECTOR(1); - -ASSERT NOT ( b = c ); - -ASSERT (a, u, b) IS_IN x; -ASSERT (a, u, c) IS_IN x; -ASSERT (d, u, a) IS_IN y; -ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv1-unit.cvc.smt2 b/test/regress/regress1/rels/bv1-unit.cvc.smt2 new file mode 100644 index 000000000..b61b9403f --- /dev/null +++ b/test/regress/regress1/rels/bv1-unit.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(declare-datatypes ((unit 0)) (((u)))) + +(declare-fun x () (Set (Tuple (_ BitVec 1) unit (_ BitVec 1)))) +(declare-fun y () (Set (Tuple (_ BitVec 1) unit (_ BitVec 1)))) +(declare-fun a () (_ BitVec 1)) +(declare-fun b () (_ BitVec 1)) +(declare-fun c () (_ BitVec 1)) +(declare-fun d () (_ BitVec 1)) +(declare-fun e () (_ BitVec 1)) +(assert (not (= b c))) +(assert (member (mkTuple a u b) x)) +(assert (member (mkTuple a u c) x)) +(assert (member (mkTuple d u a) y)) +(assert (not (member (mkTuple a u u a) (join x y)))) +(check-sat) diff --git a/test/regress/regress1/rels/bv1-unitb.cvc b/test/regress/regress1/rels/bv1-unitb.cvc deleted file mode 100644 index 0a09614a7..000000000 --- a/test/regress/regress1/rels/bv1-unitb.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -DATATYPE unitb = ub(data : BITVECTOR(1)) END; -BvPair: TYPE = [BITVECTOR(1), unitb, BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BITVECTOR(1); -b : BITVECTOR(1); -c : BITVECTOR(1); -d : BITVECTOR(1); -e : BITVECTOR(1); -u : unitb; - -ASSERT NOT ( b = c ); - -ASSERT (a, u, b) IS_IN x; -ASSERT (a, u, c) IS_IN x; -ASSERT (d, u, a) IS_IN y; -ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 new file mode 100644 index 000000000..c1db4195f --- /dev/null +++ b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 @@ -0,0 +1,19 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(declare-datatypes ((unitb 0)) (((ub (data (_ BitVec 1)))))) + +(declare-fun x () (Set (Tuple (_ BitVec 1) unitb (_ BitVec 1)))) +(declare-fun y () (Set (Tuple (_ BitVec 1) unitb (_ BitVec 1)))) +(declare-fun a () (_ BitVec 1)) +(declare-fun b () (_ BitVec 1)) +(declare-fun c () (_ BitVec 1)) +(declare-fun d () (_ BitVec 1)) +(declare-fun e () (_ BitVec 1)) +(declare-fun u () unitb) +(assert (not (= b c))) +(assert (member (mkTuple a u b) x)) +(assert (member (mkTuple a u c) x)) +(assert (member (mkTuple d u a) y)) +(assert (not (member (mkTuple a u u a) (join x y)))) +(check-sat) diff --git a/test/regress/regress1/rels/bv1.cvc b/test/regress/regress1/rels/bv1.cvc deleted file mode 100644 index 7e0f18953..000000000 --- a/test/regress/regress1/rels/bv1.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BITVECTOR(1); -b : BITVECTOR(1); -c : BITVECTOR(1); -d : BITVECTOR(1); -e : BITVECTOR(1); - -ASSERT NOT ( b = c ); - -ASSERT (a, b) IS_IN x; -ASSERT (a, c) IS_IN x; -ASSERT (d, a) IS_IN y; -ASSERT NOT ( ( a, a ) IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv1.cvc.smt2 b/test/regress/regress1/rels/bv1.cvc.smt2 new file mode 100644 index 000000000..93fa6a296 --- /dev/null +++ b/test/regress/regress1/rels/bv1.cvc.smt2 @@ -0,0 +1,17 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun a () (_ BitVec 1)) +(declare-fun b () (_ BitVec 1)) +(declare-fun c () (_ BitVec 1)) +(declare-fun d () (_ BitVec 1)) +(declare-fun e () (_ BitVec 1)) +(assert (not (= b c))) +(assert (member (mkTuple a b) x)) +(assert (member (mkTuple a c) x)) +(assert (member (mkTuple d a) y)) +(assert (not (member (mkTuple a a) (join x y)))) +(check-sat) diff --git a/test/regress/regress1/rels/bv1p-sat.cvc b/test/regress/regress1/rels/bv1p-sat.cvc deleted file mode 100644 index a48cb6407..000000000 --- a/test/regress/regress1/rels/bv1p-sat.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BvPair; -b : BvPair; -c : BvPair; -d : BvPair; - -ASSERT DISTINCT ( a, b ); -ASSERT DISTINCT ( c, d ); - -ASSERT a IS_IN x; -ASSERT b IS_IN x; -ASSERT a IS_IN y; -ASSERT b IS_IN y; -ASSERT NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)); - - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv1p-sat.cvc.smt2 b/test/regress/regress1/rels/bv1p-sat.cvc.smt2 new file mode 100644 index 000000000..a653f887b --- /dev/null +++ b/test/regress/regress1/rels/bv1p-sat.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun a () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun b () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun c () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun d () (Tuple (_ BitVec 1) (_ BitVec 1))) +(assert (distinct a b)) +(assert (distinct c d)) +(assert (member a x)) +(assert (member b x)) +(assert (member a y)) +(assert (member b y)) +(assert (let ((_let_1 (join x y))) (and (not (member c _let_1)) (not (member d _let_1))))) +(check-sat) diff --git a/test/regress/regress1/rels/bv1p.cvc b/test/regress/regress1/rels/bv1p.cvc deleted file mode 100644 index ed9fdce1f..000000000 --- a/test/regress/regress1/rels/bv1p.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% COMMAND-LINE: --jh-rlv-order -% EXPECT: unsat - -% note we require jh-rlv-order on this benchmark to avoid a proof failure currently (7/7/21) - -OPTION "logic" "ALL"; -BvPair: TYPE = [BITVECTOR(1), BITVECTOR(1)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BvPair; -b : BvPair; -c : BvPair; -d : BvPair; -e : BvPair; - -ASSERT DISTINCT ( a, b ); -ASSERT DISTINCT ( c, d, e ); - -ASSERT a IS_IN x; -ASSERT b IS_IN x; -ASSERT a IS_IN y; -ASSERT b IS_IN y; -ASSERT (NOT ( c IS_IN (x JOIN y)) AND NOT ( d IS_IN (x JOIN y)) AND NOT ( e IS_IN (x JOIN y)) ); - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv1p.cvc.smt2 b/test/regress/regress1/rels/bv1p.cvc.smt2 new file mode 100644 index 000000000..d5d9aa40f --- /dev/null +++ b/test/regress/regress1/rels/bv1p.cvc.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --jh-rlv-order +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun y () (Set (Tuple (_ BitVec 1) (_ BitVec 1)))) +(declare-fun a () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun b () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun c () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun d () (Tuple (_ BitVec 1) (_ BitVec 1))) +(declare-fun e () (Tuple (_ BitVec 1) (_ BitVec 1))) +(assert (distinct a b)) +(assert (distinct c d e)) +(assert (member a x)) +(assert (member b x)) +(assert (member a y)) +(assert (member b y)) +(assert (let ((_let_1 (join x y))) (and (and (not (member c _let_1)) (not (member d _let_1))) (not (member e _let_1))))) +(check-sat) diff --git a/test/regress/regress1/rels/bv2.cvc b/test/regress/regress1/rels/bv2.cvc deleted file mode 100644 index f3a729f2e..000000000 --- a/test/regress/regress1/rels/bv2.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -BvPair: TYPE = [BITVECTOR(2), BITVECTOR(2)]; -x : SET OF BvPair; -y : SET OF BvPair; - -a : BITVECTOR(2); -b : BITVECTOR(2); -c : BITVECTOR(2); -d : BITVECTOR(2); -e : BITVECTOR(2); - -ASSERT NOT ( b = c ); - -ASSERT (a, b) IS_IN x; -ASSERT (a, c) IS_IN x; -ASSERT (d, a) IS_IN y; -ASSERT NOT ( ( a, a ) IS_IN (x JOIN y)); - -CHECKSAT; diff --git a/test/regress/regress1/rels/bv2.cvc.smt2 b/test/regress/regress1/rels/bv2.cvc.smt2 new file mode 100644 index 000000000..824e7e125 --- /dev/null +++ b/test/regress/regress1/rels/bv2.cvc.smt2 @@ -0,0 +1,17 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple (_ BitVec 2) (_ BitVec 2)))) +(declare-fun y () (Set (Tuple (_ BitVec 2) (_ BitVec 2)))) +(declare-fun a () (_ BitVec 2)) +(declare-fun b () (_ BitVec 2)) +(declare-fun c () (_ BitVec 2)) +(declare-fun d () (_ BitVec 2)) +(declare-fun e () (_ BitVec 2)) +(assert (not (= b c))) +(assert (member (mkTuple a b) x)) +(assert (member (mkTuple a c) x)) +(assert (member (mkTuple d a) y)) +(assert (not (member (mkTuple a a) (join x y)))) +(check-sat) diff --git a/test/regress/regress1/rels/garbage_collect.cvc b/test/regress/regress1/rels/garbage_collect.cvc deleted file mode 100644 index 1fc1f2fea..000000000 --- a/test/regress/regress1/rels/garbage_collect.cvc +++ /dev/null @@ -1,60 +0,0 @@ -% EXPECT: unsat -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/regress1/rels/garbage_collect.cvc.smt2 b/test/regress/regress1/rels/garbage_collect.cvc.smt2 new file mode 100644 index 000000000..c4bba2cd3 --- /dev/null +++ b/test/regress/regress1/rels/garbage_collect.cvc.smt2 @@ -0,0 +1,37 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-sort H_TYPE 0) + +(declare-sort Obj 0) + + + + +(declare-fun h0 () (Set (Tuple H_TYPE))) +(declare-fun h1 () (Set (Tuple H_TYPE))) +(declare-fun h2 () (Set (Tuple H_TYPE))) +(declare-fun h3 () (Set (Tuple H_TYPE))) +(declare-fun s0 () H_TYPE) +(declare-fun s1 () H_TYPE) +(declare-fun s2 () H_TYPE) +(declare-fun s3 () H_TYPE) +(assert (= h0 (singleton (mkTuple s0)))) +(assert (= h1 (singleton (mkTuple s1)))) +(assert (= h2 (singleton (mkTuple s2)))) +(assert (= h3 (singleton (mkTuple s3)))) +(declare-fun ref () (Set (Tuple H_TYPE Obj Obj))) +(declare-fun mark () (Set (Tuple H_TYPE Obj))) +(declare-fun empty_obj_set () (Set (Tuple Obj))) +(assert (= empty_obj_set (as emptyset (Set (Tuple Obj))))) +(declare-fun root () Obj) +(declare-fun live () Obj) +(assert (= (join h1 mark) empty_obj_set)) +(assert (subset (join h0 ref) (join h1 ref))) +(assert (forall ((n Obj)) (=> (member (mkTuple root n) (tclosure (join h1 ref))) (member (mkTuple n) (join h2 mark))))) +(assert (subset (join h1 ref) (join h2 ref))) +(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (=> (not (member _let_1 (join h2 mark))) (= (join (singleton _let_1) (join h3 ref)) empty_obj_set))))) +(assert (forall ((n Obj)) (let ((_let_1 (mkTuple n))) (let ((_let_2 (singleton _let_1))) (=> (member _let_1 (join h2 mark)) (= (join _let_2 (join h3 ref)) (join _let_2 (join h2 ref)))))))) +(assert (member (mkTuple root live) (tclosure (join h0 ref)))) +(assert (let ((_let_1 (singleton (mkTuple live)))) (not (subset (join _let_1 (join h0 ref)) (join _let_1 (join h3 ref)))))) +(check-sat) diff --git a/test/regress/regress1/rels/iden_1_1.cvc b/test/regress/regress1/rels/iden_1_1.cvc deleted file mode 100644 index 16bf42115..000000000 --- a/test/regress/regress1/rels/iden_1_1.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: sat -OPTION "sets-ext"; -OPTION "logic" "ALL"; -Atom:TYPE; -AtomPair: TYPE = [Atom, Atom]; -x : SET OF AtomPair; -t : SET OF [Atom]; -univ : SET OF [Atom]; -univ2 : SET OF [Atom,Atom]; - -a : Atom; -b : Atom; -c : Atom; -d : Atom; -ASSERT univ = UNIVERSE::SET OF [Atom]; -ASSERT univ2 = UNIVERSE::SET OF [Atom, Atom]; -ASSERT univ2 = (univ PRODUCT univ); -ASSERT (a, b) IS_IN x; -ASSERT (c, d) IS_IN x; -ASSERT NOT(a = b); -ASSERT IDEN(univ) <= x; -CHECKSAT; diff --git a/test/regress/regress1/rels/iden_1_1.cvc.smt2 b/test/regress/regress1/rels/iden_1_1.cvc.smt2 new file mode 100644 index 000000000..eb09d698f --- /dev/null +++ b/test/regress/regress1/rels/iden_1_1.cvc.smt2 @@ -0,0 +1,22 @@ +; EXPECT: sat +(set-option :incremental false) +(set-option :sets-ext true) +(set-logic ALL) +(declare-sort Atom 0) + +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun univ () (Set (Tuple Atom))) +(declare-fun univ2 () (Set (Tuple Atom Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(assert (= univ (as univset (Set (Tuple Atom))))) +(assert (= univ2 (as univset (Set (Tuple Atom Atom))))) +(assert (= univ2 (product univ univ))) +(assert (member (mkTuple a b) x)) +(assert (member (mkTuple c d) x)) +(assert (not (= a b))) +(assert (subset (iden univ) x)) +(check-sat) diff --git a/test/regress/regress1/rels/join-eq-structure-and.cvc b/test/regress/regress1/rels/join-eq-structure-and.cvc deleted file mode 100644 index 329946c46..000000000 --- a/test/regress/regress1/rels/join-eq-structure-and.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -DATATYPE unit = u END; -IntUPair: TYPE = [INT, unit]; -UIntPair: TYPE = [unit, INT]; -w : SET OF IntUPair; -z : SET OF UIntPair; - -ASSERT (x JOIN y) = (w JOIN z) AND (x JOIN y ) = TRANSPOSE(w JOIN z); - -ASSERT (0,1) IS_IN (x JOIN y); - -t : INT; -ASSERT t >= 0 AND t <=1; -s : INT; -ASSERT s >= 0 AND s <=1; - -ASSERT s+t = 1; - -ASSERT ( s ,u ) IS_IN w; -ASSERT NOT ( u, t ) IS_IN z; - -CHECKSAT; diff --git a/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 new file mode 100644 index 000000000..1eb1419c8 --- /dev/null +++ b/test/regress/regress1/rels/join-eq-structure-and.cvc.smt2 @@ -0,0 +1,21 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-datatypes ((unit 0)) (((u)))) + + +(declare-fun w () (Set (Tuple Int unit))) +(declare-fun z () (Set (Tuple unit Int))) +(assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (and (= _let_2 _let_1) (= _let_2 (transpose _let_1)))))) +(assert (member (mkTuple 0 1) (join x y))) +(declare-fun t () Int) +(assert (and (>= t 0) (<= t 1))) +(declare-fun s () Int) +(assert (and (>= s 0) (<= s 1))) +(assert (= (+ s t) 1)) +(assert (member (mkTuple s u) w)) +(assert (not (member (mkTuple u t) z))) +(check-sat) diff --git a/test/regress/regress1/rels/join-eq-structure.cvc b/test/regress/regress1/rels/join-eq-structure.cvc deleted file mode 100644 index 3cfb309c9..000000000 --- a/test/regress/regress1/rels/join-eq-structure.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -DATATYPE unit = u END; -IntUPair: TYPE = [INT, unit]; -UIntPair: TYPE = [unit, INT]; -w : SET OF IntUPair; -z : SET OF UIntPair; - -ASSERT (x JOIN y) = (w JOIN z) OR (x JOIN y ) = TRANSPOSE(w JOIN z); - -ASSERT (0,1) IS_IN (x JOIN y); - -t : INT; -ASSERT t >= 0 AND t <=1; -s : INT; -ASSERT s >= 0 AND s <=1; - -ASSERT s+t = 1; - -ASSERT ( s ,u ) IS_IN w; -ASSERT NOT ( u, t ) IS_IN z; - -CHECKSAT; diff --git a/test/regress/regress1/rels/join-eq-structure.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure.cvc.smt2 new file mode 100644 index 000000000..5144ac4c2 --- /dev/null +++ b/test/regress/regress1/rels/join-eq-structure.cvc.smt2 @@ -0,0 +1,21 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-datatypes ((unit 0)) (((u)))) + + +(declare-fun w () (Set (Tuple Int unit))) +(declare-fun z () (Set (Tuple unit Int))) +(assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (or (= _let_2 _let_1) (= _let_2 (transpose _let_1)))))) +(assert (member (mkTuple 0 1) (join x y))) +(declare-fun t () Int) +(assert (and (>= t 0) (<= t 1))) +(declare-fun s () Int) +(assert (and (>= s 0) (<= s 1))) +(assert (= (+ s t) 1)) +(assert (member (mkTuple s u) w)) +(assert (not (member (mkTuple u t) z))) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc b/test/regress/regress1/rels/joinImg_0_1.cvc deleted file mode 100644 index 789e36a92..000000000 --- a/test/regress/regress1/rels/joinImg_0_1.cvc +++ /dev/null @@ -1,36 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -OPTION "sets-ext"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -t : SET OF [INT]; -u : SET OF [INT]; - -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: INT; - -ASSERT (1, 7) IS_IN x; -ASSERT z IS_IN x; - -ASSERT (7, 5) IS_IN y; - -ASSERT t = (x JOIN_IMAGE 2); - -ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); - -ASSERT u = (x JOIN_IMAGE 1); - -ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); - -ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 new file mode 100644 index 000000000..8a28b74ae --- /dev/null +++ b/test/regress/regress1/rels/joinImg_0_1.cvc.smt2 @@ -0,0 +1,28 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun t () (Set (Tuple Int))) +(declare-fun u () (Set (Tuple Int))) +(declare-fun z () (Tuple Int Int)) +(assert (= z (mkTuple 1 2))) +(declare-fun zt () (Tuple Int Int)) +(assert (= zt (mkTuple 2 1))) +(declare-fun v () (Tuple Int Int)) +(assert (= v (mkTuple 1 1))) +(declare-fun a () (Tuple Int Int)) +(assert (= a (mkTuple 1 5))) +(declare-fun b () Int) +(assert (member (mkTuple 1 7) x)) +(assert (member z x)) +(assert (member (mkTuple 7 5) y)) +(assert (= t (join_image x 2))) +(assert (member (mkTuple 3) (join_image x 2))) +(assert (= u (join_image x 1))) +(assert (member (mkTuple 4) (join_image x 2))) +(assert (member (mkTuple b) (join_image x 1))) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_0_2.cvc b/test/regress/regress1/rels/joinImg_0_2.cvc deleted file mode 100644 index 89d767c7f..000000000 --- a/test/regress/regress1/rels/joinImg_0_2.cvc +++ /dev/null @@ -1,39 +0,0 @@ -% EXPECT: sat -OPTION "sets-ext"; -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -r : SET OF IntPair; - -t : SET OF [INT]; -u : SET OF [INT]; -univ : SET OF [INT]; - -z : IntPair; -ASSERT z = (1,2); -zt : IntPair; -ASSERT zt = (2,1); -s : IntPair; -ASSERT s = (1,1); -a : IntPair; -ASSERT a = (1,5); -b: INT; - -ASSERT (1, 7) IS_IN x; -ASSERT z IS_IN x; - -ASSERT (7, 5) IS_IN y; - -ASSERT t = (x JOIN_IMAGE 2); -ASSERT univ = (x JOIN_IMAGE 0); -ASSERT TUPLE(100) IS_IN t; - -ASSERT NOT (TUPLE(3) IS_IN univ); - -ASSERT u = (x JOIN_IMAGE 1); - -ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); - -ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 new file mode 100644 index 000000000..8f1954c10 --- /dev/null +++ b/test/regress/regress1/rels/joinImg_0_2.cvc.smt2 @@ -0,0 +1,31 @@ +; EXPECT: sat +(set-option :incremental false) +(set-option :sets-ext true) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun t () (Set (Tuple Int))) +(declare-fun u () (Set (Tuple Int))) +(declare-fun univ () (Set (Tuple Int))) +(declare-fun z () (Tuple Int Int)) +(assert (= z (mkTuple 1 2))) +(declare-fun zt () (Tuple Int Int)) +(assert (= zt (mkTuple 2 1))) +(declare-fun s () (Tuple Int Int)) +(assert (= s (mkTuple 1 1))) +(declare-fun a () (Tuple Int Int)) +(assert (= a (mkTuple 1 5))) +(declare-fun b () Int) +(assert (member (mkTuple 1 7) x)) +(assert (member z x)) +(assert (member (mkTuple 7 5) y)) +(assert (= t (join_image x 2))) +(assert (= univ (join_image x 0))) +(assert (member (mkTuple 100) t)) +(assert (not (member (mkTuple 3) univ))) +(assert (= u (join_image x 1))) +(assert (member (mkTuple 4) (join_image x 2))) +(assert (member (mkTuple b) (join_image x 1))) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_1.cvc b/test/regress/regress1/rels/joinImg_1.cvc deleted file mode 100644 index 1849ffb84..000000000 --- a/test/regress/regress1/rels/joinImg_1.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -OPTION "sets-ext"; -Atom: TYPE; -x : SET OF [Atom, Atom]; -y : SET OF [Atom, Atom]; -r : SET OF [Atom, Atom]; - -t : SET OF [Atom]; - -a : Atom; -b : Atom; -c : Atom; -d : Atom; -e : Atom; - -ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); -ASSERT x = {(b, c), (d, e), (c, e)}; -ASSERT NOT(a = b); - -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1.cvc.smt2 new file mode 100644 index 000000000..3c5664d76 --- /dev/null +++ b/test/regress/regress1/rels/joinImg_1.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) +(declare-sort Atom 0) +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun y () (Set (Tuple Atom Atom))) +(declare-fun r () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(declare-fun e () Atom) +(assert (member (mkTuple a) (join_image x 2))) +(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (not (= a b))) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_1_1.cvc b/test/regress/regress1/rels/joinImg_1_1.cvc deleted file mode 100644 index 748b57062..000000000 --- a/test/regress/regress1/rels/joinImg_1_1.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -OPTION "sets-ext"; -Atom: TYPE; -x : SET OF [Atom, Atom]; -y : SET OF [Atom, Atom]; -r : SET OF [Atom, Atom]; - -t : SET OF [Atom]; - -a : Atom; -b : Atom; -c : Atom; -d : Atom; -e : Atom; - -ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); -ASSERT t = (x JOIN_IMAGE 2); -ASSERT x = {(b, c), (d, e), (c, e)}; -ASSERT TUPLE(c) IS_IN t; - -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 new file mode 100644 index 000000000..c8e228f1b --- /dev/null +++ b/test/regress/regress1/rels/joinImg_1_1.cvc.smt2 @@ -0,0 +1,19 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) +(declare-sort Atom 0) +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun y () (Set (Tuple Atom Atom))) +(declare-fun r () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(declare-fun e () Atom) +(assert (member (mkTuple a) (join_image x 2))) +(assert (= t (join_image x 2))) +(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (member (mkTuple c) t)) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_2.cvc b/test/regress/regress1/rels/joinImg_2.cvc deleted file mode 100644 index 2ce3f3f69..000000000 --- a/test/regress/regress1/rels/joinImg_2.cvc +++ /dev/null @@ -1,34 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -OPTION "sets-ext"; -Atom: TYPE; -x : SET OF [Atom, Atom]; -y : SET OF [Atom, Atom]; -r : SET OF [Atom, Atom]; - -t : SET OF [Atom]; - -a : Atom; -b : Atom; -c : Atom; -d : Atom; -e : Atom; -f : Atom; -g : Atom; - -ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); -ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 3); -%ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; -ASSERT x = {(f, g), (b, c), (d, e), (c, e), (f, b)}; -ASSERT (a, f) IS_IN x; -ASSERT (a, f) IS_IN y; -ASSERT x = y; - - - -ASSERT NOT(a = b); - -ASSERT NOT (TUPLE(d) IS_IN (x JOIN_IMAGE 2)); -ASSERT f = d; - -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_2.cvc.smt2 b/test/regress/regress1/rels/joinImg_2.cvc.smt2 new file mode 100644 index 000000000..9f8efdfff --- /dev/null +++ b/test/regress/regress1/rels/joinImg_2.cvc.smt2 @@ -0,0 +1,26 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) +(declare-sort Atom 0) +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun y () (Set (Tuple Atom Atom))) +(declare-fun r () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(declare-fun e () Atom) +(declare-fun f () Atom) +(declare-fun g () Atom) +(assert (member (mkTuple a) (join_image x 2))) +(assert (member (mkTuple a) (join_image y 3))) +(assert (= x (union (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))) (singleton (mkTuple f b))))) +(assert (member (mkTuple a f) x)) +(assert (member (mkTuple a f) y)) +(assert (= x y)) +(assert (not (= a b))) +(assert (not (member (mkTuple d) (join_image x 2)))) +(assert (= f d)) +(check-sat) diff --git a/test/regress/regress1/rels/joinImg_2_1.cvc b/test/regress/regress1/rels/joinImg_2_1.cvc deleted file mode 100644 index 0238b253f..000000000 --- a/test/regress/regress1/rels/joinImg_2_1.cvc +++ /dev/null @@ -1,25 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -OPTION "sets-ext"; -Atom: TYPE; -x : SET OF [Atom, Atom]; -y : SET OF [Atom, Atom]; -r : SET OF [Atom, Atom]; - -t : SET OF [Atom]; - -a : Atom; -b : Atom; -c : Atom; -d : Atom; -e : Atom; -f : Atom; -g : Atom; - -ASSERT TUPLE(a) IS_IN (x JOIN_IMAGE 2); -ASSERT TUPLE(a) IS_IN (y JOIN_IMAGE 1); -ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; -ASSERT x = {(f, g), (b, c), (d, e), (c, e)}; -ASSERT (NOT(a = b)) OR (NOT(a = f)); - -CHECKSAT; diff --git a/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 new file mode 100644 index 000000000..797e7b35b --- /dev/null +++ b/test/regress/regress1/rels/joinImg_2_1.cvc.smt2 @@ -0,0 +1,22 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) +(declare-sort Atom 0) +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun y () (Set (Tuple Atom Atom))) +(declare-fun r () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(declare-fun e () Atom) +(declare-fun f () Atom) +(declare-fun g () Atom) +(assert (member (mkTuple a) (join_image x 2))) +(assert (member (mkTuple a) (join_image y 1))) +(assert (= y (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (= x (union (union (union (singleton (mkTuple f g)) (singleton (mkTuple b c))) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (or (not (= a b)) (not (= a f)))) +(check-sat) diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc b/test/regress/regress1/rels/prod-mod-eq.cvc deleted file mode 100644 index 0e6a00fb4..000000000 --- a/test/regress/regress1/rels/prod-mod-eq.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -IntPairPair: TYPE = [INT, INT, INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPairPair; -z1 : SET OF IntPair; -w1 : SET OF IntPair; -z2 : SET OF IntPair; -w2 : SET OF IntPair; - -%ASSERT NOT (0,1,2,3) IS_IN (x PRODUCT y); - -ASSERT NOT( z = (x PRODUCT y) ); - -ASSERT (0,1,2,3) IS_IN z; - -ASSERT (0,1) IS_IN z1; -ASSERT (0,1) IS_IN z2; -ASSERT (2,3) IS_IN w1; -ASSERT (2,3) IS_IN w2; - -ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 ); - -CHECKSAT; diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 new file mode 100644 index 000000000..7d9147a8b --- /dev/null +++ b/test/regress/regress1/rels/prod-mod-eq.cvc.smt2 @@ -0,0 +1,20 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int Int Int))) +(declare-fun z1 () (Set (Tuple Int Int))) +(declare-fun w1 () (Set (Tuple Int Int))) +(declare-fun z2 () (Set (Tuple Int Int))) +(declare-fun w2 () (Set (Tuple Int Int))) +(assert (not (= z (product x y)))) +(assert (member (mkTuple 0 1 2 3) z)) +(assert (member (mkTuple 0 1) z1)) +(assert (member (mkTuple 0 1) z2)) +(assert (member (mkTuple 2 3) w1)) +(assert (member (mkTuple 2 3) w2)) +(assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2)))) +(check-sat) diff --git a/test/regress/regress1/rels/prod-mod-eq2.cvc b/test/regress/regress1/rels/prod-mod-eq2.cvc deleted file mode 100644 index 871b1b7d7..000000000 --- a/test/regress/regress1/rels/prod-mod-eq2.cvc +++ /dev/null @@ -1,26 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -IntPairPair: TYPE = [INT, INT, INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPairPair; -z1 : SET OF IntPair; -w1 : SET OF IntPair; -z2 : SET OF IntPair; -w2 : SET OF IntPair; -P : SET OF IntPairPair -> BOOLEAN; - -ASSERT z = (x PRODUCT y); - -ASSERT P( z ); -ASSERT NOT P( {(0,1,2,3)} ); - -ASSERT (0,1) IS_IN z1; -ASSERT (0,1) IS_IN z2; -ASSERT (2,3) IS_IN w1; -ASSERT (2,3) IS_IN w2; - -ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 ); - -CHECKSAT; diff --git a/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 new file mode 100644 index 000000000..b2bee8b3f --- /dev/null +++ b/test/regress/regress1/rels/prod-mod-eq2.cvc.smt2 @@ -0,0 +1,22 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int Int Int))) +(declare-fun z1 () (Set (Tuple Int Int))) +(declare-fun w1 () (Set (Tuple Int Int))) +(declare-fun z2 () (Set (Tuple Int Int))) +(declare-fun w2 () (Set (Tuple Int Int))) +(declare-fun P ((Set (Tuple Int Int Int Int))) Bool) +(assert (= z (product x y))) +(assert (P z)) +(assert (not (P (singleton (mkTuple 0 1 2 3))))) +(assert (member (mkTuple 0 1) z1)) +(assert (member (mkTuple 0 1) z2)) +(assert (member (mkTuple 2 3) w1)) +(assert (member (mkTuple 2 3) w2)) +(assert (or (and (= x z1) (= y w1)) (and (= x z2) (= y w2)))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_complex_3.cvc b/test/regress/regress1/rels/rel_complex_3.cvc deleted file mode 100644 index 94639eff0..000000000 --- a/test/regress/regress1/rels/rel_complex_3.cvc +++ /dev/null @@ -1,49 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 new file mode 100644 index 000000000..ccd152268 --- /dev/null +++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 @@ -0,0 +1,36 @@ +; EXPECT: unsat +(set-option :incremental true) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(declare-fun f () (Tuple Int Int)) +(assert (= f (mkTuple 3 1))) +(assert (member f x)) +(declare-fun g () (Tuple Int Int)) +(assert (= g (mkTuple 1 3))) +(assert (member g y)) +(declare-fun h () (Tuple Int Int)) +(assert (= h (mkTuple 3 5))) +(assert (member h x)) +(assert (member h y)) +(assert (= r (join x y))) +(declare-fun e () (Tuple Int Int)) +(assert (not (member e r))) +(assert (not (= z (intersection x y)))) +(assert (= z (setminus x y))) +(assert (subset x y)) +(assert (member e (join r z))) +(assert (member e x)) +(assert (member e (intersection x y))) +(push 1) + +(assert true) + +(check-sat) + +(pop 1) + diff --git a/test/regress/regress1/rels/rel_complex_4.cvc b/test/regress/regress1/rels/rel_complex_4.cvc deleted file mode 100644 index d75bf0cd4..000000000 --- a/test/regress/regress1/rels/rel_complex_4.cvc +++ /dev/null @@ -1,52 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 new file mode 100644 index 000000000..1f99668ac --- /dev/null +++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 @@ -0,0 +1,40 @@ +; EXPECT: unsat +(set-option :incremental true) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(declare-fun f () (Tuple Int Int)) +(assert (= f (mkTuple 3 1))) +(assert (member f x)) +(declare-fun g () (Tuple Int Int)) +(assert (= g (mkTuple 1 3))) +(assert (member g y)) +(declare-fun h () (Tuple Int Int)) +(assert (= h (mkTuple 3 5))) +(assert (member h x)) +(assert (member h y)) +(assert (= r (join x y))) +(declare-fun a () Int) +(declare-fun e () (Tuple Int Int)) +(assert (= e (mkTuple a a))) +(assert (= w (singleton e))) +(assert (subset (transpose w) y)) +(assert (not (member e r))) +(assert (not (= z (intersection x y)))) +(assert (= z (setminus x y))) +(assert (subset x y)) +(assert (member e (join r z))) +(assert (member e x)) +(assert (member e (intersection x y))) +(push 1) + +(assert true) + +(check-sat) + +(pop 1) + diff --git a/test/regress/regress1/rels/rel_complex_5.cvc b/test/regress/regress1/rels/rel_complex_5.cvc deleted file mode 100644 index 27225e72c..000000000 --- a/test/regress/regress1/rels/rel_complex_5.cvc +++ /dev/null @@ -1,55 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 new file mode 100644 index 000000000..dfbc23c8e --- /dev/null +++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 @@ -0,0 +1,42 @@ +; EXPECT: unsat +(set-option :incremental true) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(declare-fun f () (Tuple Int Int)) +(assert (= f (mkTuple 3 1))) +(assert (member f x)) +(declare-fun g () (Tuple Int Int)) +(assert (= g (mkTuple 1 3))) +(assert (member g y)) +(declare-fun h () (Tuple Int Int)) +(assert (= h (mkTuple 3 5))) +(assert (member h x)) +(assert (member h y)) +(assert (= r (join x y))) +(declare-fun a () (Tuple Int)) +(assert (= a (mkTuple 1))) +(declare-fun e () (Tuple Int Int)) +(assert (= e (mkTuple 1 1))) +(assert (let ((_let_1 (singleton a))) (= w (product _let_1 _let_1)))) +(assert (subset (transpose w) y)) +(assert (not (member e r))) +(assert (not (= z (intersection x y)))) +(assert (= z (setminus x y))) +(assert (subset x y)) +(assert (member e (join r z))) +(assert (member e x)) +(assert (member e (intersection x y))) +(push 1) + +(assert true) + +(check-sat) + +(pop 1) + diff --git a/test/regress/regress1/rels/rel_mix_0_1.cvc b/test/regress/regress1/rels/rel_mix_0_1.cvc deleted file mode 100644 index 75f4965f2..000000000 --- a/test/regress/regress1/rels/rel_mix_0_1.cvc +++ /dev/null @@ -1,30 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_mix_0_1.cvc.smt2 b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 new file mode 100644 index 000000000..08323ed5a --- /dev/null +++ b/test/regress/regress1/rels/rel_mix_0_1.cvc.smt2 @@ -0,0 +1,23 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int))) +(declare-fun z () (Set (Tuple Int))) +(declare-fun r2 () (Set (Tuple Int Int))) +(declare-fun d () (Tuple Int Int)) +(assert (= d (mkTuple 1 3))) +(assert (member (mkTuple 1 3) y)) +(declare-fun a () (Tuple Int Int)) +(assert (member a x)) +(declare-fun e () (Tuple Int Int)) +(assert (= e (mkTuple 4 3))) +(assert (= r (join x y))) +(assert (= r2 (product w z))) +(assert (not (member e r))) +(assert (not (= r r2))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc b/test/regress/regress1/rels/rel_pressure_0.cvc deleted file mode 100644 index 5648b7ba8..000000000 --- a/test/regress/regress1/rels/rel_pressure_0.cvc +++ /dev/null @@ -1,617 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_pressure_0.cvc.smt2 b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 new file mode 100644 index 000000000..698f2f5d9 --- /dev/null +++ b/test/regress/regress1/rels/rel_pressure_0.cvc.smt2 @@ -0,0 +1,614 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(declare-fun a11 () (Tuple Int Int)) +(assert (= a11 (mkTuple 1 1))) +(assert (member a11 x)) +(declare-fun a12 () (Tuple Int Int)) +(assert (= a12 (mkTuple 1 2))) +(assert (member a12 x)) +(declare-fun a13 () (Tuple Int Int)) +(assert (= a13 (mkTuple 1 3))) +(assert (member a13 x)) +(declare-fun a14 () (Tuple Int Int)) +(assert (= a14 (mkTuple 1 4))) +(assert (member a14 x)) +(declare-fun a15 () (Tuple Int Int)) +(assert (= a15 (mkTuple 1 5))) +(assert (member a15 x)) +(declare-fun a16 () (Tuple Int Int)) +(assert (= a16 (mkTuple 1 6))) +(assert (member a16 x)) +(declare-fun a17 () (Tuple Int Int)) +(assert (= a17 (mkTuple 1 7))) +(assert (member a17 x)) +(declare-fun a18 () (Tuple Int Int)) +(assert (= a18 (mkTuple 1 8))) +(assert (member a18 x)) +(declare-fun a19 () (Tuple Int Int)) +(assert (= a19 (mkTuple 1 9))) +(assert (member a19 x)) +(declare-fun a110 () (Tuple Int Int)) +(assert (= a110 (mkTuple 1 10))) +(assert (member a110 x)) +(declare-fun a21 () (Tuple Int Int)) +(assert (= a21 (mkTuple 2 1))) +(assert (member a21 x)) +(declare-fun a22 () (Tuple Int Int)) +(assert (= a22 (mkTuple 2 2))) +(assert (member a22 x)) +(declare-fun a23 () (Tuple Int Int)) +(assert (= a23 (mkTuple 2 3))) +(assert (member a23 x)) +(declare-fun a24 () (Tuple Int Int)) +(assert (= a24 (mkTuple 2 4))) +(assert (member a24 x)) +(declare-fun a25 () (Tuple Int Int)) +(assert (= a25 (mkTuple 2 5))) +(assert (member a25 x)) +(declare-fun a26 () (Tuple Int Int)) +(assert (= a26 (mkTuple 2 6))) +(assert (member a26 x)) +(declare-fun a27 () (Tuple Int Int)) +(assert (= a27 (mkTuple 2 7))) +(assert (member a27 x)) +(declare-fun a28 () (Tuple Int Int)) +(assert (= a28 (mkTuple 2 8))) +(assert (member a28 x)) +(declare-fun a29 () (Tuple Int Int)) +(assert (= a29 (mkTuple 2 9))) +(assert (member a29 x)) +(declare-fun a210 () (Tuple Int Int)) +(assert (= a210 (mkTuple 2 10))) +(assert (member a210 x)) +(declare-fun a31 () (Tuple Int Int)) +(assert (= a31 (mkTuple 3 1))) +(assert (member a31 x)) +(declare-fun a32 () (Tuple Int Int)) +(assert (= a32 (mkTuple 3 2))) +(assert (member a32 x)) +(declare-fun a33 () (Tuple Int Int)) +(assert (= a33 (mkTuple 3 3))) +(assert (member a33 x)) +(declare-fun a34 () (Tuple Int Int)) +(assert (= a34 (mkTuple 3 4))) +(assert (member a34 x)) +(declare-fun a35 () (Tuple Int Int)) +(assert (= a35 (mkTuple 3 5))) +(assert (member a35 x)) +(declare-fun a36 () (Tuple Int Int)) +(assert (= a36 (mkTuple 3 6))) +(assert (member a36 x)) +(declare-fun a37 () (Tuple Int Int)) +(assert (= a37 (mkTuple 3 7))) +(assert (member a37 x)) +(declare-fun a38 () (Tuple Int Int)) +(assert (= a38 (mkTuple 3 8))) +(assert (member a38 x)) +(declare-fun a39 () (Tuple Int Int)) +(assert (= a39 (mkTuple 3 9))) +(assert (member a39 x)) +(declare-fun a310 () (Tuple Int Int)) +(assert (= a310 (mkTuple 3 10))) +(assert (member a310 x)) +(declare-fun a41 () (Tuple Int Int)) +(assert (= a41 (mkTuple 4 1))) +(assert (member a41 x)) +(declare-fun a42 () (Tuple Int Int)) +(assert (= a42 (mkTuple 4 2))) +(assert (member a42 x)) +(declare-fun a43 () (Tuple Int Int)) +(assert (= a43 (mkTuple 4 3))) +(assert (member a43 x)) +(declare-fun a44 () (Tuple Int Int)) +(assert (= a44 (mkTuple 4 4))) +(assert (member a44 x)) +(declare-fun a45 () (Tuple Int Int)) +(assert (= a45 (mkTuple 4 5))) +(assert (member a45 x)) +(declare-fun a46 () (Tuple Int Int)) +(assert (= a46 (mkTuple 4 6))) +(assert (member a46 x)) +(declare-fun a47 () (Tuple Int Int)) +(assert (= a47 (mkTuple 4 7))) +(assert (member a47 x)) +(declare-fun a48 () (Tuple Int Int)) +(assert (= a48 (mkTuple 4 8))) +(assert (member a48 x)) +(declare-fun a49 () (Tuple Int Int)) +(assert (= a49 (mkTuple 4 9))) +(assert (member a49 x)) +(declare-fun a410 () (Tuple Int Int)) +(assert (= a410 (mkTuple 4 10))) +(assert (member a410 x)) +(declare-fun a51 () (Tuple Int Int)) +(assert (= a51 (mkTuple 5 1))) +(assert (member a51 x)) +(declare-fun a52 () (Tuple Int Int)) +(assert (= a52 (mkTuple 5 2))) +(assert (member a52 x)) +(declare-fun a53 () (Tuple Int Int)) +(assert (= a53 (mkTuple 5 3))) +(assert (member a53 x)) +(declare-fun a54 () (Tuple Int Int)) +(assert (= a54 (mkTuple 5 4))) +(assert (member a54 x)) +(declare-fun a55 () (Tuple Int Int)) +(assert (= a55 (mkTuple 5 5))) +(assert (member a55 x)) +(declare-fun a56 () (Tuple Int Int)) +(assert (= a56 (mkTuple 5 6))) +(assert (member a56 x)) +(declare-fun a57 () (Tuple Int Int)) +(assert (= a57 (mkTuple 5 7))) +(assert (member a57 x)) +(declare-fun a58 () (Tuple Int Int)) +(assert (= a58 (mkTuple 5 8))) +(assert (member a58 x)) +(declare-fun a59 () (Tuple Int Int)) +(assert (= a59 (mkTuple 5 9))) +(assert (member a59 x)) +(declare-fun a510 () (Tuple Int Int)) +(assert (= a510 (mkTuple 5 10))) +(assert (member a510 x)) +(declare-fun a61 () (Tuple Int Int)) +(assert (= a61 (mkTuple 6 1))) +(assert (member a61 x)) +(declare-fun a62 () (Tuple Int Int)) +(assert (= a62 (mkTuple 6 2))) +(assert (member a62 x)) +(declare-fun a63 () (Tuple Int Int)) +(assert (= a63 (mkTuple 6 3))) +(assert (member a63 x)) +(declare-fun a64 () (Tuple Int Int)) +(assert (= a64 (mkTuple 6 4))) +(assert (member a64 x)) +(declare-fun a65 () (Tuple Int Int)) +(assert (= a65 (mkTuple 6 5))) +(assert (member a65 x)) +(declare-fun a66 () (Tuple Int Int)) +(assert (= a66 (mkTuple 6 6))) +(assert (member a66 x)) +(declare-fun a67 () (Tuple Int Int)) +(assert (= a67 (mkTuple 6 7))) +(assert (member a67 x)) +(declare-fun a68 () (Tuple Int Int)) +(assert (= a68 (mkTuple 6 8))) +(assert (member a68 x)) +(declare-fun a69 () (Tuple Int Int)) +(assert (= a69 (mkTuple 6 9))) +(assert (member a69 x)) +(declare-fun a610 () (Tuple Int Int)) +(assert (= a610 (mkTuple 6 10))) +(assert (member a610 x)) +(declare-fun a71 () (Tuple Int Int)) +(assert (= a71 (mkTuple 7 1))) +(assert (member a71 x)) +(declare-fun a72 () (Tuple Int Int)) +(assert (= a72 (mkTuple 7 2))) +(assert (member a72 x)) +(declare-fun a73 () (Tuple Int Int)) +(assert (= a73 (mkTuple 7 3))) +(assert (member a73 x)) +(declare-fun a74 () (Tuple Int Int)) +(assert (= a74 (mkTuple 7 4))) +(assert (member a74 x)) +(declare-fun a75 () (Tuple Int Int)) +(assert (= a75 (mkTuple 7 5))) +(assert (member a75 x)) +(declare-fun a76 () (Tuple Int Int)) +(assert (= a76 (mkTuple 7 6))) +(assert (member a76 x)) +(declare-fun a77 () (Tuple Int Int)) +(assert (= a77 (mkTuple 7 7))) +(assert (member a77 x)) +(declare-fun a78 () (Tuple Int Int)) +(assert (= a78 (mkTuple 7 8))) +(assert (member a78 x)) +(declare-fun a79 () (Tuple Int Int)) +(assert (= a79 (mkTuple 7 9))) +(assert (member a79 x)) +(declare-fun a710 () (Tuple Int Int)) +(assert (= a710 (mkTuple 7 10))) +(assert (member a710 x)) +(declare-fun a81 () (Tuple Int Int)) +(assert (= a81 (mkTuple 8 1))) +(assert (member a81 x)) +(declare-fun a82 () (Tuple Int Int)) +(assert (= a82 (mkTuple 8 2))) +(assert (member a82 x)) +(declare-fun a83 () (Tuple Int Int)) +(assert (= a83 (mkTuple 8 3))) +(assert (member a83 x)) +(declare-fun a84 () (Tuple Int Int)) +(assert (= a84 (mkTuple 8 4))) +(assert (member a84 x)) +(declare-fun a85 () (Tuple Int Int)) +(assert (= a85 (mkTuple 8 5))) +(assert (member a85 x)) +(declare-fun a86 () (Tuple Int Int)) +(assert (= a86 (mkTuple 8 6))) +(assert (member a86 x)) +(declare-fun a87 () (Tuple Int Int)) +(assert (= a87 (mkTuple 8 7))) +(assert (member a87 x)) +(declare-fun a88 () (Tuple Int Int)) +(assert (= a88 (mkTuple 8 8))) +(assert (member a88 x)) +(declare-fun a89 () (Tuple Int Int)) +(assert (= a89 (mkTuple 8 9))) +(assert (member a89 x)) +(declare-fun a810 () (Tuple Int Int)) +(assert (= a810 (mkTuple 8 10))) +(assert (member a810 x)) +(declare-fun a91 () (Tuple Int Int)) +(assert (= a91 (mkTuple 9 1))) +(assert (member a91 x)) +(declare-fun a92 () (Tuple Int Int)) +(assert (= a92 (mkTuple 9 2))) +(assert (member a92 x)) +(declare-fun a93 () (Tuple Int Int)) +(assert (= a93 (mkTuple 9 3))) +(assert (member a93 x)) +(declare-fun a94 () (Tuple Int Int)) +(assert (= a94 (mkTuple 9 4))) +(assert (member a94 x)) +(declare-fun a95 () (Tuple Int Int)) +(assert (= a95 (mkTuple 9 5))) +(assert (member a95 x)) +(declare-fun a96 () (Tuple Int Int)) +(assert (= a96 (mkTuple 9 6))) +(assert (member a96 x)) +(declare-fun a97 () (Tuple Int Int)) +(assert (= a97 (mkTuple 9 7))) +(assert (member a97 x)) +(declare-fun a98 () (Tuple Int Int)) +(assert (= a98 (mkTuple 9 8))) +(assert (member a98 x)) +(declare-fun a99 () (Tuple Int Int)) +(assert (= a99 (mkTuple 9 9))) +(assert (member a99 x)) +(declare-fun a910 () (Tuple Int Int)) +(assert (= a910 (mkTuple 9 10))) +(assert (member a910 x)) +(declare-fun a101 () (Tuple Int Int)) +(assert (= a101 (mkTuple 10 1))) +(assert (member a101 x)) +(declare-fun a102 () (Tuple Int Int)) +(assert (= a102 (mkTuple 10 2))) +(assert (member a102 x)) +(declare-fun a103 () (Tuple Int Int)) +(assert (= a103 (mkTuple 10 3))) +(assert (member a103 x)) +(declare-fun a104 () (Tuple Int Int)) +(assert (= a104 (mkTuple 10 4))) +(assert (member a104 x)) +(declare-fun a105 () (Tuple Int Int)) +(assert (= a105 (mkTuple 10 5))) +(assert (member a105 x)) +(declare-fun a106 () (Tuple Int Int)) +(assert (= a106 (mkTuple 10 6))) +(assert (member a106 x)) +(declare-fun a107 () (Tuple Int Int)) +(assert (= a107 (mkTuple 10 7))) +(assert (member a107 x)) +(declare-fun a108 () (Tuple Int Int)) +(assert (= a108 (mkTuple 10 8))) +(assert (member a108 x)) +(declare-fun a109 () (Tuple Int Int)) +(assert (= a109 (mkTuple 10 9))) +(assert (member a109 x)) +(declare-fun a1010 () (Tuple Int Int)) +(assert (= a1010 (mkTuple 10 10))) +(assert (member a1010 x)) +(declare-fun b11 () (Tuple Int Int)) +(assert (= b11 (mkTuple 1 1))) +(assert (member b11 y)) +(declare-fun b12 () (Tuple Int Int)) +(assert (= b12 (mkTuple 1 2))) +(assert (member b12 y)) +(declare-fun b13 () (Tuple Int Int)) +(assert (= b13 (mkTuple 1 3))) +(assert (member b13 y)) +(declare-fun b14 () (Tuple Int Int)) +(assert (= b14 (mkTuple 1 4))) +(assert (member b14 y)) +(declare-fun b15 () (Tuple Int Int)) +(assert (= b15 (mkTuple 1 5))) +(assert (member b15 y)) +(declare-fun b16 () (Tuple Int Int)) +(assert (= b16 (mkTuple 1 6))) +(assert (member b16 y)) +(declare-fun b17 () (Tuple Int Int)) +(assert (= b17 (mkTuple 1 7))) +(assert (member b17 y)) +(declare-fun b18 () (Tuple Int Int)) +(assert (= b18 (mkTuple 1 8))) +(assert (member b18 y)) +(declare-fun b19 () (Tuple Int Int)) +(assert (= b19 (mkTuple 1 9))) +(assert (member b19 y)) +(declare-fun b110 () (Tuple Int Int)) +(assert (= b110 (mkTuple 1 10))) +(assert (member b110 y)) +(declare-fun b21 () (Tuple Int Int)) +(assert (= b21 (mkTuple 2 1))) +(assert (member b21 y)) +(declare-fun b22 () (Tuple Int Int)) +(assert (= b22 (mkTuple 2 2))) +(assert (member b22 y)) +(declare-fun b23 () (Tuple Int Int)) +(assert (= b23 (mkTuple 2 3))) +(assert (member b23 y)) +(declare-fun b24 () (Tuple Int Int)) +(assert (= b24 (mkTuple 2 4))) +(assert (member b24 y)) +(declare-fun b25 () (Tuple Int Int)) +(assert (= b25 (mkTuple 2 5))) +(assert (member b25 y)) +(declare-fun b26 () (Tuple Int Int)) +(assert (= b26 (mkTuple 2 6))) +(assert (member b26 y)) +(declare-fun b27 () (Tuple Int Int)) +(assert (= b27 (mkTuple 2 7))) +(assert (member b27 y)) +(declare-fun b28 () (Tuple Int Int)) +(assert (= b28 (mkTuple 2 8))) +(assert (member b28 y)) +(declare-fun b29 () (Tuple Int Int)) +(assert (= b29 (mkTuple 2 9))) +(assert (member b29 y)) +(declare-fun b210 () (Tuple Int Int)) +(assert (= b210 (mkTuple 2 10))) +(assert (member b210 y)) +(declare-fun b31 () (Tuple Int Int)) +(assert (= b31 (mkTuple 3 1))) +(assert (member b31 y)) +(declare-fun b32 () (Tuple Int Int)) +(assert (= b32 (mkTuple 3 2))) +(assert (member b32 y)) +(declare-fun b33 () (Tuple Int Int)) +(assert (= b33 (mkTuple 3 3))) +(assert (member b33 y)) +(declare-fun b34 () (Tuple Int Int)) +(assert (= b34 (mkTuple 3 4))) +(assert (member b34 y)) +(declare-fun b35 () (Tuple Int Int)) +(assert (= b35 (mkTuple 3 5))) +(assert (member b35 y)) +(declare-fun b36 () (Tuple Int Int)) +(assert (= b36 (mkTuple 3 6))) +(assert (member b36 y)) +(declare-fun b37 () (Tuple Int Int)) +(assert (= b37 (mkTuple 3 7))) +(assert (member b37 y)) +(declare-fun b38 () (Tuple Int Int)) +(assert (= b38 (mkTuple 3 8))) +(assert (member b38 y)) +(declare-fun b39 () (Tuple Int Int)) +(assert (= b39 (mkTuple 3 9))) +(assert (member b39 y)) +(declare-fun b310 () (Tuple Int Int)) +(assert (= b310 (mkTuple 3 10))) +(assert (member b310 y)) +(declare-fun b41 () (Tuple Int Int)) +(assert (= b41 (mkTuple 4 1))) +(assert (member b41 y)) +(declare-fun b42 () (Tuple Int Int)) +(assert (= b42 (mkTuple 4 2))) +(assert (member b42 y)) +(declare-fun b43 () (Tuple Int Int)) +(assert (= b43 (mkTuple 4 3))) +(assert (member b43 y)) +(declare-fun b44 () (Tuple Int Int)) +(assert (= b44 (mkTuple 4 4))) +(assert (member b44 y)) +(declare-fun b45 () (Tuple Int Int)) +(assert (= b45 (mkTuple 4 5))) +(assert (member b45 y)) +(declare-fun b46 () (Tuple Int Int)) +(assert (= b46 (mkTuple 4 6))) +(assert (member b46 y)) +(declare-fun b47 () (Tuple Int Int)) +(assert (= b47 (mkTuple 4 7))) +(assert (member b47 y)) +(declare-fun b48 () (Tuple Int Int)) +(assert (= b48 (mkTuple 4 8))) +(assert (member b48 y)) +(declare-fun b49 () (Tuple Int Int)) +(assert (= b49 (mkTuple 4 9))) +(assert (member b49 y)) +(declare-fun b410 () (Tuple Int Int)) +(assert (= b410 (mkTuple 4 10))) +(assert (member b410 y)) +(declare-fun b51 () (Tuple Int Int)) +(assert (= b51 (mkTuple 5 1))) +(assert (member b51 y)) +(declare-fun b52 () (Tuple Int Int)) +(assert (= b52 (mkTuple 5 2))) +(assert (member b52 y)) +(declare-fun b53 () (Tuple Int Int)) +(assert (= b53 (mkTuple 5 3))) +(assert (member b53 y)) +(declare-fun b54 () (Tuple Int Int)) +(assert (= b54 (mkTuple 5 4))) +(assert (member b54 y)) +(declare-fun b55 () (Tuple Int Int)) +(assert (= b55 (mkTuple 5 5))) +(assert (member b55 y)) +(declare-fun b56 () (Tuple Int Int)) +(assert (= b56 (mkTuple 5 6))) +(assert (member b56 y)) +(declare-fun b57 () (Tuple Int Int)) +(assert (= b57 (mkTuple 5 7))) +(assert (member b57 y)) +(declare-fun b58 () (Tuple Int Int)) +(assert (= b58 (mkTuple 5 8))) +(assert (member b58 y)) +(declare-fun b59 () (Tuple Int Int)) +(assert (= b59 (mkTuple 5 9))) +(assert (member b59 y)) +(declare-fun b510 () (Tuple Int Int)) +(assert (= b510 (mkTuple 5 10))) +(assert (member b510 y)) +(declare-fun b61 () (Tuple Int Int)) +(assert (= b61 (mkTuple 6 1))) +(assert (member b61 y)) +(declare-fun b62 () (Tuple Int Int)) +(assert (= b62 (mkTuple 6 2))) +(assert (member b62 y)) +(declare-fun b63 () (Tuple Int Int)) +(assert (= b63 (mkTuple 6 3))) +(assert (member b63 y)) +(declare-fun b64 () (Tuple Int Int)) +(assert (= b64 (mkTuple 6 4))) +(assert (member b64 y)) +(declare-fun b65 () (Tuple Int Int)) +(assert (= b65 (mkTuple 6 5))) +(assert (member b65 y)) +(declare-fun b66 () (Tuple Int Int)) +(assert (= b66 (mkTuple 6 6))) +(assert (member b66 y)) +(declare-fun b67 () (Tuple Int Int)) +(assert (= b67 (mkTuple 6 7))) +(assert (member b67 y)) +(declare-fun b68 () (Tuple Int Int)) +(assert (= b68 (mkTuple 6 8))) +(assert (member b68 y)) +(declare-fun b69 () (Tuple Int Int)) +(assert (= b69 (mkTuple 6 9))) +(assert (member b69 y)) +(declare-fun b610 () (Tuple Int Int)) +(assert (= b610 (mkTuple 6 10))) +(assert (member b610 y)) +(declare-fun b71 () (Tuple Int Int)) +(assert (= b71 (mkTuple 7 1))) +(assert (member b71 y)) +(declare-fun b72 () (Tuple Int Int)) +(assert (= b72 (mkTuple 7 2))) +(assert (member b72 y)) +(declare-fun b73 () (Tuple Int Int)) +(assert (= b73 (mkTuple 7 3))) +(assert (member b73 y)) +(declare-fun b74 () (Tuple Int Int)) +(assert (= b74 (mkTuple 7 4))) +(assert (member b74 y)) +(declare-fun b75 () (Tuple Int Int)) +(assert (= b75 (mkTuple 7 5))) +(assert (member b75 y)) +(declare-fun b76 () (Tuple Int Int)) +(assert (= b76 (mkTuple 7 6))) +(assert (member b76 y)) +(declare-fun b77 () (Tuple Int Int)) +(assert (= b77 (mkTuple 7 7))) +(assert (member b77 y)) +(declare-fun b78 () (Tuple Int Int)) +(assert (= b78 (mkTuple 7 8))) +(assert (member b78 y)) +(declare-fun b79 () (Tuple Int Int)) +(assert (= b79 (mkTuple 7 9))) +(assert (member b79 y)) +(declare-fun b710 () (Tuple Int Int)) +(assert (= b710 (mkTuple 7 10))) +(assert (member b710 y)) +(declare-fun b81 () (Tuple Int Int)) +(assert (= b81 (mkTuple 8 1))) +(assert (member b81 y)) +(declare-fun b82 () (Tuple Int Int)) +(assert (= b82 (mkTuple 8 2))) +(assert (member b82 y)) +(declare-fun b83 () (Tuple Int Int)) +(assert (= b83 (mkTuple 8 3))) +(assert (member b83 y)) +(declare-fun b84 () (Tuple Int Int)) +(assert (= b84 (mkTuple 8 4))) +(assert (member b84 y)) +(declare-fun b85 () (Tuple Int Int)) +(assert (= b85 (mkTuple 8 5))) +(assert (member b85 y)) +(declare-fun b86 () (Tuple Int Int)) +(assert (= b86 (mkTuple 8 6))) +(assert (member b86 y)) +(declare-fun b87 () (Tuple Int Int)) +(assert (= b87 (mkTuple 8 7))) +(assert (member b87 y)) +(declare-fun b88 () (Tuple Int Int)) +(assert (= b88 (mkTuple 8 8))) +(assert (member b88 y)) +(declare-fun b89 () (Tuple Int Int)) +(assert (= b89 (mkTuple 8 9))) +(assert (member b89 y)) +(declare-fun b810 () (Tuple Int Int)) +(assert (= b810 (mkTuple 8 10))) +(assert (member b810 y)) +(declare-fun b91 () (Tuple Int Int)) +(assert (= b91 (mkTuple 9 1))) +(assert (member b91 y)) +(declare-fun b92 () (Tuple Int Int)) +(assert (= b92 (mkTuple 9 2))) +(assert (member b92 y)) +(declare-fun b93 () (Tuple Int Int)) +(assert (= b93 (mkTuple 9 3))) +(assert (member b93 y)) +(declare-fun b94 () (Tuple Int Int)) +(assert (= b94 (mkTuple 9 4))) +(assert (member b94 y)) +(declare-fun b95 () (Tuple Int Int)) +(assert (= b95 (mkTuple 9 5))) +(assert (member b95 y)) +(declare-fun b96 () (Tuple Int Int)) +(assert (= b96 (mkTuple 9 6))) +(assert (member b96 y)) +(declare-fun b97 () (Tuple Int Int)) +(assert (= b97 (mkTuple 9 7))) +(assert (member b97 y)) +(declare-fun b98 () (Tuple Int Int)) +(assert (= b98 (mkTuple 9 8))) +(assert (member b98 y)) +(declare-fun b99 () (Tuple Int Int)) +(assert (= b99 (mkTuple 9 9))) +(assert (member b99 y)) +(declare-fun b910 () (Tuple Int Int)) +(assert (= b910 (mkTuple 9 10))) +(assert (member b910 y)) +(declare-fun b101 () (Tuple Int Int)) +(assert (= b101 (mkTuple 10 1))) +(assert (member b101 y)) +(declare-fun b102 () (Tuple Int Int)) +(assert (= b102 (mkTuple 10 2))) +(assert (member b102 y)) +(declare-fun b103 () (Tuple Int Int)) +(assert (= b103 (mkTuple 10 3))) +(assert (member b103 y)) +(declare-fun b104 () (Tuple Int Int)) +(assert (= b104 (mkTuple 10 4))) +(assert (member b104 y)) +(declare-fun b105 () (Tuple Int Int)) +(assert (= b105 (mkTuple 10 5))) +(assert (member b105 y)) +(declare-fun b106 () (Tuple Int Int)) +(assert (= b106 (mkTuple 10 6))) +(assert (member b106 y)) +(declare-fun b107 () (Tuple Int Int)) +(assert (= b107 (mkTuple 10 7))) +(assert (member b107 y)) +(declare-fun b108 () (Tuple Int Int)) +(assert (= b108 (mkTuple 10 8))) +(assert (member b108 y)) +(declare-fun b109 () (Tuple Int Int)) +(assert (= b109 (mkTuple 10 9))) +(assert (member b109 y)) +(declare-fun b1010 () (Tuple Int Int)) +(assert (= b1010 (mkTuple 10 10))) +(assert (member b1010 y)) +(assert (member (mkTuple 1 9) z)) +(declare-fun a () (Tuple Int Int)) +(assert (= a (mkTuple 9 1))) +(assert (= r (join (join (transpose x) y) z))) +(assert (not (member a (transpose r)))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_10_1.cvc b/test/regress/regress1/rels/rel_tc_10_1.cvc deleted file mode 100644 index 391b58bfb..000000000 --- a/test/regress/regress1/rels/rel_tc_10_1.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_10_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 new file mode 100644 index 000000000..32d670b25 --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_10_1.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(assert (= a c)) +(assert (= a d)) +(assert (member (mkTuple 1 c) x)) +(assert (member (mkTuple 2 d) x)) +(assert (member (mkTuple a 5) y)) +(assert (= y (tclosure x))) +(assert (member (mkTuple 2 5) y)) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_4.cvc b/test/regress/regress1/rels/rel_tc_4.cvc deleted file mode 100644 index b194902cb..000000000 --- a/test/regress/regress1/rels/rel_tc_4.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_4.cvc.smt2 b/test/regress/regress1/rels/rel_tc_4.cvc.smt2 new file mode 100644 index 000000000..29cb0609f --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_4.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(assert (member (mkTuple 1 a) x)) +(assert (member (mkTuple 1 c) x)) +(assert (member (mkTuple 1 d) x)) +(assert (member (mkTuple b 1) x)) +(assert (= b d)) +(assert (member (mkTuple 2 b) (join (join x x) x))) +(assert (not (member (mkTuple 2 1) (tclosure x)))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_4_1.cvc b/test/regress/regress1/rels/rel_tc_4_1.cvc deleted file mode 100644 index 6dae90f80..000000000 --- a/test/regress/regress1/rels/rel_tc_4_1.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_4_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_4_1.cvc.smt2 new file mode 100644 index 000000000..7e0ce99c5 --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_4_1.cvc.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(assert (= y (join (tclosure x) x))) +(assert (not (= y (tclosure x)))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_5_1.cvc b/test/regress/regress1/rels/rel_tc_5_1.cvc deleted file mode 100644 index d49a19217..000000000 --- a/test/regress/regress1/rels/rel_tc_5_1.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_5_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_5_1.cvc.smt2 new file mode 100644 index 000000000..a57fe6e81 --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_5_1.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(assert (= y (tclosure x))) +(assert (not (= y (join (join x x) x)))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_6.cvc b/test/regress/regress1/rels/rel_tc_6.cvc deleted file mode 100644 index b751dc201..000000000 --- a/test/regress/regress1/rels/rel_tc_6.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_6.cvc.smt2 b/test/regress/regress1/rels/rel_tc_6.cvc.smt2 new file mode 100644 index 000000000..dd584b122 --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_6.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(assert (= y (tclosure x))) +(assert (not (subset (join (join x x) x) y))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tc_9_1.cvc b/test/regress/regress1/rels/rel_tc_9_1.cvc deleted file mode 100644 index af7bbb044..000000000 --- a/test/regress/regress1/rels/rel_tc_9_1.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tc_9_1.cvc.smt2 b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 new file mode 100644 index 000000000..599d30946 --- /dev/null +++ b/test/regress/regress1/rels/rel_tc_9_1.cvc.smt2 @@ -0,0 +1,22 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(assert (= z (tclosure x))) +(assert (= w (join x y))) +(assert (member (mkTuple 2 2) z)) +(assert (member (mkTuple 0 3) y)) +(assert (member (mkTuple (- 1) 3) y)) +(assert (member (mkTuple 1 3) y)) +(assert (member (mkTuple (- 2) 3) y)) +(assert (member (mkTuple 2 3) y)) +(assert (member (mkTuple 3 3) y)) +(assert (member (mkTuple 4 3) y)) +(assert (member (mkTuple 5 3) y)) +(assert (not (member (mkTuple 2 3) (join x y)))) +(assert (not (member (mkTuple 2 1) x))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tp_2.cvc b/test/regress/regress1/rels/rel_tp_2.cvc deleted file mode 100644 index 73702ea8e..000000000 --- a/test/regress/regress1/rels/rel_tp_2.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tp_2.cvc.smt2 b/test/regress/regress1/rels/rel_tp_2.cvc.smt2 new file mode 100644 index 000000000..822c1fd52 --- /dev/null +++ b/test/regress/regress1/rels/rel_tp_2.cvc.smt2 @@ -0,0 +1,11 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(assert (or (= z (transpose y)) (= z (transpose x)))) +(assert (not (= (transpose z) y))) +(assert (not (= (transpose z) x))) +(check-sat) diff --git a/test/regress/regress1/rels/rel_tp_join_2_1.cvc b/test/regress/regress1/rels/rel_tp_join_2_1.cvc deleted file mode 100644 index 51d6c1050..000000000 --- a/test/regress/regress1/rels/rel_tp_join_2_1.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -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/regress1/rels/rel_tp_join_2_1.cvc.smt2 b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 new file mode 100644 index 000000000..1a71721ac --- /dev/null +++ b/test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun r () (Set (Tuple Int Int))) +(assert (member (mkTuple 7 1) x)) +(assert (member (mkTuple 2 3) x)) +(assert (member (mkTuple 7 3) y)) +(assert (member (mkTuple 4 7) y)) +(assert (member (mkTuple 3 4) z)) +(declare-fun a () (Tuple Int Int)) +(assert (= a (mkTuple 4 1))) +(assert (= r (join (join (transpose x) y) z))) +(assert (member a (transpose r))) +(check-sat) diff --git a/test/regress/regress1/rels/set-strat.cvc b/test/regress/regress1/rels/set-strat.cvc deleted file mode 100644 index c56a2b16e..000000000 --- a/test/regress/regress1/rels/set-strat.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [ INT, INT]; -SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ]; -x : SET OF IntPair; -y : SET OF IntPair; -w : SET OF IntPair; -z : SET OF SetIntPair; - -a : IntPair; -b : IntPair; - -ASSERT NOT a = b; - -ASSERT a IS_IN x; -ASSERT b IS_IN y; -ASSERT b IS_IN w; -ASSERT (x,y) IS_IN z; -ASSERT (w,x) IS_IN z; -ASSERT NOT ( (x,x) IS_IN (z JOIN z) ); - -ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z); - -CHECKSAT; diff --git a/test/regress/regress1/rels/set-strat.cvc.smt2 b/test/regress/regress1/rels/set-strat.cvc.smt2 new file mode 100644 index 000000000..e1c82de24 --- /dev/null +++ b/test/regress/regress1/rels/set-strat.cvc.smt2 @@ -0,0 +1,20 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple Int Int))) +(declare-fun y () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(declare-fun z () (Set (Tuple (Set (Tuple Int Int)) (Set (Tuple Int Int))))) +(declare-fun a () (Tuple Int Int)) +(declare-fun b () (Tuple Int Int)) +(assert (not (= a b))) +(assert (member a x)) +(assert (member b y)) +(assert (member b w)) +(assert (member (mkTuple x y) z)) +(assert (member (mkTuple w x) z)) +(assert (not (member (mkTuple x x) (join z z)))) +(assert (member (mkTuple x (singleton (mkTuple 0 0))) (join z z))) +(check-sat) diff --git a/test/regress/regress1/rels/strat.cvc b/test/regress/regress1/rels/strat.cvc deleted file mode 100644 index dc5c2f37d..000000000 --- a/test/regress/regress1/rels/strat.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [ INT, INT]; -IntIntPair: TYPE = [ IntPair, IntPair]; -x : SET OF IntIntPair; -y : SET OF IntIntPair; -z : SET OF IntPair; -w : SET OF IntPair; - -a : IntPair; -b : IntPair; -c : IntIntPair; - -ASSERT NOT a = b; - -ASSERT a IS_IN z; -ASSERT b IS_IN z; -ASSERT (a,b) IS_IN x; -ASSERT (b,a) IS_IN x; -ASSERT c IS_IN x; -ASSERT NOT ( c = (a,b) ) AND NOT ( c = (b,a) ); - - -CHECKSAT; diff --git a/test/regress/regress1/rels/strat.cvc.smt2 b/test/regress/regress1/rels/strat.cvc.smt2 new file mode 100644 index 000000000..0cc6905f2 --- /dev/null +++ b/test/regress/regress1/rels/strat.cvc.smt2 @@ -0,0 +1,20 @@ +; EXPECT: sat +(set-option :incremental false) +(set-logic ALL) + + +(declare-fun x () (Set (Tuple (Tuple Int Int) (Tuple Int Int)))) +(declare-fun y () (Set (Tuple (Tuple Int Int) (Tuple Int Int)))) +(declare-fun z () (Set (Tuple Int Int))) +(declare-fun w () (Set (Tuple Int Int))) +(declare-fun a () (Tuple Int Int)) +(declare-fun b () (Tuple Int Int)) +(declare-fun c () (Tuple (Tuple Int Int) (Tuple Int Int))) +(assert (not (= a b))) +(assert (member a z)) +(assert (member b z)) +(assert (member (mkTuple a b) x)) +(assert (member (mkTuple b a) x)) +(assert (member c x)) +(assert (and (not (= c (mkTuple a b))) (not (= c (mkTuple b a))))) +(check-sat) |