diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
commit | 031722bee8682005bd4c8700ef78b5f893fc48fe (patch) | |
tree | 46a936a1bd20ea2cc588df0d3205cf7eb0fd4177 /test/regress/regress0/rels | |
parent | e79e64329ce7d6df0003cab28dadb9b8bcc6f9ca (diff) |
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Diffstat (limited to 'test/regress/regress0/rels')
83 files changed, 2660 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/Makefile b/test/regress/regress0/rels/Makefile new file mode 100644 index 000000000..bd7dc8797 --- /dev/null +++ b/test/regress/regress0/rels/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/rels + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am new file mode 100644 index 000000000..6b8fdfec7 --- /dev/null +++ b/test/regress/regress0/rels/Makefile.am @@ -0,0 +1,115 @@ +SUBDIRS = . + +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + addr_book_0.cvc \ + bv2.cvc \ + oneLoc_no_quant-int_0_1.cvc \ + rel_complex_5.cvc \ + rel_join_3_1.cvc \ + rel_product_0_1.cvc \ + rel_tc_10_1.cvc \ + rel_tc_6.cvc \ + rel_tp_join_2_1.cvc \ + rel_transpose_1_1.cvc \ + strat_0_1.cvc \ + addr_book_1_1.cvc \ + prod-mod-eq2.cvc \ + rel_conflict_0.cvc \ + rel_join_3.cvc \ + rel_product_0.cvc \ + rel_tc_11.cvc \ + rel_tc_7.cvc \ + rel_tp_join_2.cvc \ + rel_transpose_1.cvc \ + strat.cvc \ + addr_book_1.cvc \ + join-eq-structure_0_1.cvc \ + prod-mod-eq.cvc \ + rel_join_0_1.cvc \ + rel_join_4.cvc \ + rel_product_1_1.cvc \ + rel_tc_2_1.cvc \ + rel_tp_join_3.cvc \ + rel_transpose_3.cvc \ + bv1.cvc \ + join-eq-structure-and.cvc \ + rel_1tup_0.cvc \ + rel_join_0.cvc \ + rel_join_5.cvc \ + rel_product_1.cvc \ + rel_tc_3_1.cvc \ + rel_tc_9_1.cvc \ + rel_tp_join_eq_0.cvc \ + rel_transpose_4.cvc \ + bv1p.cvc \ + join-eq-structure.cvc \ + rel_complex_0.cvc \ + rel_join_1_1.cvc \ + rel_join_6.cvc \ + rel_symbolic_1_1.cvc \ + rel_tc_3.cvc \ + rel_tp_2.cvc \ + rel_tp_join_int_0.cvc \ + rel_transpose_5.cvc \ + bv1p-sat.cvc \ + join-eq-u.cvc \ + rel_complex_1.cvc \ + rel_join_1.cvc \ + rel_join_7.cvc \ + rel_symbolic_1.cvc \ + rel_tc_4_1.cvc \ + rel_tp_3_1.cvc \ + rel_tp_join_pro_0.cvc \ + rel_transpose_6.cvc \ + bv1-unitb.cvc \ + join-eq-u-sat.cvc \ + rel_complex_3.cvc \ + rel_join_2_1.cvc \ + rel_mix_0_1.cvc \ + rel_symbolic_2_1.cvc \ + rel_tc_4.cvc \ + rel_tp_join_0.cvc \ + rel_tp_join_var_0.cvc \ + rel_transpose_7.cvc \ + bv1-unit.cvc \ + rel_complex_4.cvc \ + rel_join_2.cvc \ + rel_pressure_0.cvc \ + rel_symbolic_3_1.cvc \ + rel_tc_5_1.cvc \ + rel_tp_join_1.cvc \ + rel_transpose_0.cvc \ + set-strat.cvc + +# unsolved : garbage_collect.cvc +# dump-unsat-core crash : rel_tc_8.cvc + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/rels/addr_book_0.cvc b/test/regress/regress0/rels/addr_book_0.cvc new file mode 100644 index 000000000..5b1ecefd8 --- /dev/null +++ b/test/regress/regress0/rels/addr_book_0.cvc @@ -0,0 +1,49 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom : TYPE; +AtomTup : TYPE = [Atom]; +AtomBinTup : TYPE = [Atom, Atom]; +AtomTerTup : TYPE = [Atom, Atom, Atom]; +Target: SET OF AtomTup; + +Name: SET OF AtomTup; +Addr: SET OF AtomTup; +Book: SET OF AtomTup; +names: SET OF AtomBinTup; +addr: SET OF AtomTerTup; + +b1: Atom; +b1_tup : AtomTup; +ASSERT b1_tup = TUPLE(b1); +ASSERT b1_tup IS_IN Book; + +b2: Atom; +b2_tup : AtomTup; +ASSERT b2_tup = TUPLE(b2); +ASSERT b2_tup IS_IN Book; + +b3: Atom; +b3_tup : AtomTup; +ASSERT b3_tup = TUPLE(b3); +ASSERT b3_tup IS_IN Book; + +n: Atom; +n_tup : AtomTup; +ASSERT n_tup = TUPLE(n); +ASSERT n_tup IS_IN Name; + +t: Atom; +t_tup : AtomTup; +ASSERT t_tup = TUPLE(t); +ASSERT t_tup IS_IN Target; + +ASSERT ((Book JOIN addr) JOIN Target) <= Name; +ASSERT (Book JOIN names) <= Name; +ASSERT (Name & Addr) = {}::SET OF AtomTup; + +ASSERT ({n_tup} JOIN ({b1_tup} JOIN addr)) = {}::SET OF AtomTup; +ASSERT ({n_tup} JOIN ({b2_tup} JOIN addr)) = ({n_tup} JOIN ({b1_tup} JOIN addr)) | {t_tup}; +ASSERT ({n_tup} JOIN ({b3_tup} JOIN addr)) = ({n_tup} JOIN ({b2_tup} JOIN addr)) - {t_tup}; +ASSERT NOT (({n_tup} JOIN ({b1_tup} JOIN addr)) = ({n_tup} JOIN ({b3_tup} JOIN addr))); + +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/rels/addr_book_1.cvc b/test/regress/regress0/rels/addr_book_1.cvc new file mode 100644 index 000000000..34176f274 --- /dev/null +++ b/test/regress/regress0/rels/addr_book_1.cvc @@ -0,0 +1,45 @@ +% 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/rels/addr_book_1_1.cvc b/test/regress/regress0/rels/addr_book_1_1.cvc new file mode 100644 index 000000000..3273ade3a --- /dev/null +++ b/test/regress/regress0/rels/addr_book_1_1.cvc @@ -0,0 +1,45 @@ +% EXPECT: sat +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/rels/bv1-unit.cvc b/test/regress/regress0/rels/bv1-unit.cvc new file mode 100644 index 000000000..970ebdc8c --- /dev/null +++ b/test/regress/regress0/rels/bv1-unit.cvc @@ -0,0 +1,21 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/bv1-unitb.cvc b/test/regress/regress0/rels/bv1-unitb.cvc new file mode 100644 index 000000000..50a5bb48a --- /dev/null +++ b/test/regress/regress0/rels/bv1-unitb.cvc @@ -0,0 +1,22 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/bv1.cvc b/test/regress/regress0/rels/bv1.cvc new file mode 100644 index 000000000..95e7419ba --- /dev/null +++ b/test/regress/regress0/rels/bv1.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/bv1p-sat.cvc b/test/regress/regress0/rels/bv1p-sat.cvc new file mode 100644 index 000000000..5eceb214c --- /dev/null +++ b/test/regress/regress0/rels/bv1p-sat.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/bv1p.cvc b/test/regress/regress0/rels/bv1p.cvc new file mode 100644 index 000000000..130ccae97 --- /dev/null +++ b/test/regress/regress0/rels/bv1p.cvc @@ -0,0 +1,22 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/bv2.cvc b/test/regress/regress0/rels/bv2.cvc new file mode 100644 index 000000000..d7162de7c --- /dev/null +++ b/test/regress/regress0/rels/bv2.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/garbage_collect.cvc b/test/regress/regress0/rels/garbage_collect.cvc new file mode 100644 index 000000000..1fc1f2fea --- /dev/null +++ b/test/regress/regress0/rels/garbage_collect.cvc @@ -0,0 +1,60 @@ +% 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/regress0/rels/join-eq-structure-and.cvc b/test/regress/regress0/rels/join-eq-structure-and.cvc new file mode 100644 index 000000000..177410b1e --- /dev/null +++ b/test/regress/regress0/rels/join-eq-structure-and.cvc @@ -0,0 +1,26 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/join-eq-structure.cvc b/test/regress/regress0/rels/join-eq-structure.cvc new file mode 100644 index 000000000..e27d3811c --- /dev/null +++ b/test/regress/regress0/rels/join-eq-structure.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/join-eq-structure_0_1.cvc b/test/regress/regress0/rels/join-eq-structure_0_1.cvc new file mode 100644 index 000000000..e27d3811c --- /dev/null +++ b/test/regress/regress0/rels/join-eq-structure_0_1.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +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/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc new file mode 100644 index 000000000..0202cbb41 --- /dev/null +++ b/test/regress/regress0/rels/join-eq-u-sat.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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); + +ASSERT (0,1) IS_IN (x JOIN y); +ASSERT (0,u) IS_IN w; + +t : INT; +ASSERT t > 0 AND t < 3; + +ASSERT NOT (u, t ) IS_IN z; + +CHECKSAT; diff --git a/test/regress/regress0/rels/join-eq-u.cvc b/test/regress/regress0/rels/join-eq-u.cvc new file mode 100644 index 000000000..4bc498aec --- /dev/null +++ b/test/regress/regress0/rels/join-eq-u.cvc @@ -0,0 +1,22 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +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); + +ASSERT (0,1) IS_IN (x JOIN y); +ASSERT (0,u) IS_IN w; + +t : INT; +ASSERT t > 0 AND t < 2; + +ASSERT NOT (u, t ) IS_IN z; + +CHECKSAT; diff --git a/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc new file mode 100644 index 000000000..f39c23438 --- /dev/null +++ b/test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc @@ -0,0 +1,19 @@ +% EXPECT: sat +OPTION "logic" "QF_UFDTFS"; +DATATYPE Atom = atom END; + + +t : SET OF [Atom, Atom]; +b : Atom; +a : Atom; +c : Atom; +J : ( SET OF [Atom], SET OF [Atom, Atom] ) -> SET OF [Atom]; +T : SET OF [Atom, Atom] -> SET OF [Atom, Atom]; + +%ASSERT t = {} :: SET OF [Atom, Atom]; + + +ASSERT ({TUPLE(a)} JOIN t) = J({TUPLE(a)}, t); +ASSERT NOT( ({TUPLE(c)} JOIN TCLOSURE(t)) = {TUPLE(c)} ); + +CHECKSAT; diff --git a/test/regress/regress0/rels/prod-mod-eq.cvc b/test/regress/regress0/rels/prod-mod-eq.cvc new file mode 100644 index 000000000..96ef2ffba --- /dev/null +++ b/test/regress/regress0/rels/prod-mod-eq.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/prod-mod-eq2.cvc b/test/regress/regress0/rels/prod-mod-eq2.cvc new file mode 100644 index 000000000..b9341a216 --- /dev/null +++ b/test/regress/regress0/rels/prod-mod-eq2.cvc @@ -0,0 +1,26 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/rel_1tup_0.cvc b/test/regress/regress0/rels/rel_1tup_0.cvc new file mode 100644 index 000000000..50d4defd5 --- /dev/null +++ b/test/regress/regress0/rels/rel_1tup_0.cvc @@ -0,0 +1,24 @@ +% 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/rels/rel_complex_0.cvc b/test/regress/regress0/rels/rel_complex_0.cvc new file mode 100644 index 000000000..dcb753973 --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_0.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +z : 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/rels/rel_complex_1.cvc b/test/regress/regress0/rels/rel_complex_1.cvc new file mode 100644 index 000000000..969d0d71c --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_1.cvc @@ -0,0 +1,34 @@ +% 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/rels/rel_complex_3.cvc b/test/regress/regress0/rels/rel_complex_3.cvc new file mode 100644 index 000000000..492c94432 --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_3.cvc @@ -0,0 +1,49 @@ +% 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/rels/rel_complex_4.cvc b/test/regress/regress0/rels/rel_complex_4.cvc new file mode 100644 index 000000000..f473b00aa --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_4.cvc @@ -0,0 +1,52 @@ +% 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/rels/rel_complex_5.cvc b/test/regress/regress0/rels/rel_complex_5.cvc new file mode 100644 index 000000000..d64817187 --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_5.cvc @@ -0,0 +1,55 @@ +% 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/rels/rel_conflict_0.cvc b/test/regress/regress0/rels/rel_conflict_0.cvc new file mode 100644 index 000000000..c1b82339f --- /dev/null +++ b/test/regress/regress0/rels/rel_conflict_0.cvc @@ -0,0 +1,10 @@ +% 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/rels/rel_join_0.cvc b/test/regress/regress0/rels/rel_join_0.cvc new file mode 100644 index 000000000..406b8d312 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_0.cvc @@ -0,0 +1,24 @@ +% 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/rels/rel_join_0_1.cvc b/test/regress/regress0/rels/rel_join_0_1.cvc new file mode 100644 index 000000000..a7fa7efb9 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_0_1.cvc @@ -0,0 +1,27 @@ +% 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/rels/rel_join_1.cvc b/test/regress/regress0/rels/rel_join_1.cvc new file mode 100644 index 000000000..c8921afb9 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_join_1_1.cvc b/test/regress/regress0/rels/rel_join_1_1.cvc new file mode 100644 index 000000000..75fc08387 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_1_1.cvc @@ -0,0 +1,31 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +z : IntPair; +ASSERT z = (1,2); +zt : IntPair; +ASSERT zt = (2,1); +v : IntPair; +ASSERT v = (1,1); +a : IntPair; +ASSERT a = (1,5); + +ASSERT (1, 7) IS_IN x; +ASSERT (2, 3) IS_IN x; +ASSERT (3, 4) IS_IN x; + +ASSERT (7, 5) IS_IN y; +ASSERT (7, 3) IS_IN y; +ASSERT (4, 7) IS_IN y; + +%ASSERT (a IS_IN (r JOIN(x JOIN y))); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; +ASSERT r = (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_join_2.cvc b/test/regress/regress0/rels/rel_join_2.cvc new file mode 100644 index 000000000..cac7ce84d --- /dev/null +++ b/test/regress/regress0/rels/rel_join_2.cvc @@ -0,0 +1,20 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT NOT (a IS_IN (x JOIN y)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_join_2_1.cvc b/test/regress/regress0/rels/rel_join_2_1.cvc new file mode 100644 index 000000000..3e27b9cc5 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_2_1.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntTup; + +z : IntPair; +ASSERT z = (1,2); +zt : IntTup; +ASSERT zt = (2,1,3); +a : IntTup; +ASSERT a = (1,1,3); + +ASSERT z IS_IN x; +ASSERT zt IS_IN y; + +ASSERT a IS_IN (x JOIN y); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_join_3.cvc b/test/regress/regress0/rels/rel_join_3.cvc new file mode 100644 index 000000000..6e190cecf --- /dev/null +++ b/test/regress/regress0/rels/rel_join_3.cvc @@ -0,0 +1,29 @@ +% 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/rels/rel_join_3_1.cvc b/test/regress/regress0/rels/rel_join_3_1.cvc new file mode 100644 index 000000000..dedc4ae44 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_3_1.cvc @@ -0,0 +1,29 @@ +% 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 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/rels/rel_join_4.cvc b/test/regress/regress0/rels/rel_join_4.cvc new file mode 100644 index 000000000..030810f3d --- /dev/null +++ b/test/regress/regress0/rels/rel_join_4.cvc @@ -0,0 +1,32 @@ +% 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/rels/rel_join_5.cvc b/test/regress/regress0/rels/rel_join_5.cvc new file mode 100644 index 000000000..5209d8131 --- /dev/null +++ b/test/regress/regress0/rels/rel_join_5.cvc @@ -0,0 +1,19 @@ +% 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/rels/rel_join_6.cvc b/test/regress/regress0/rels/rel_join_6.cvc new file mode 100644 index 000000000..17318872f --- /dev/null +++ b/test/regress/regress0/rels/rel_join_6.cvc @@ -0,0 +1,13 @@ +% 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/rels/rel_join_7.cvc b/test/regress/regress0/rels/rel_join_7.cvc new file mode 100644 index 000000000..fff5b6efe --- /dev/null +++ b/test/regress/regress0/rels/rel_join_7.cvc @@ -0,0 +1,26 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +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/rels/rel_mix_0_1.cvc b/test/regress/regress0/rels/rel_mix_0_1.cvc new file mode 100644 index 000000000..723a9b2e2 --- /dev/null +++ b/test/regress/regress0/rels/rel_mix_0_1.cvc @@ -0,0 +1,30 @@ +% 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/rels/rel_pressure_0.cvc b/test/regress/regress0/rels/rel_pressure_0.cvc new file mode 100644 index 000000000..6cdf03600 --- /dev/null +++ b/test/regress/regress0/rels/rel_pressure_0.cvc @@ -0,0 +1,617 @@ +% 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/rels/rel_product_0.cvc b/test/regress/regress0/rels/rel_product_0.cvc new file mode 100644 index 000000000..09981be0b --- /dev/null +++ b/test/regress/regress0/rels/rel_product_0.cvc @@ -0,0 +1,20 @@ +% 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/rels/rel_product_0_1.cvc b/test/regress/regress0/rels/rel_product_0_1.cvc new file mode 100644 index 000000000..f141c7bd4 --- /dev/null +++ b/test/regress/regress0/rels/rel_product_0_1.cvc @@ -0,0 +1,20 @@ +% 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/rels/rel_product_1.cvc b/test/regress/regress0/rels/rel_product_1.cvc new file mode 100644 index 000000000..1826e5a75 --- /dev/null +++ b/test/regress/regress0/rels/rel_product_1.cvc @@ -0,0 +1,20 @@ +% 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/rels/rel_product_1_1.cvc b/test/regress/regress0/rels/rel_product_1_1.cvc new file mode 100644 index 000000000..2d79cbc0c --- /dev/null +++ b/test/regress/regress0/rels/rel_product_1_1.cvc @@ -0,0 +1,21 @@ +% 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/rels/rel_symbolic_1.cvc b/test/regress/regress0/rels/rel_symbolic_1.cvc new file mode 100644 index 000000000..08ed32411 --- /dev/null +++ b/test/regress/regress0/rels/rel_symbolic_1.cvc @@ -0,0 +1,21 @@ +% 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/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/rels/rel_symbolic_1_1.cvc new file mode 100644 index 000000000..df2d7f412 --- /dev/null +++ b/test/regress/regress0/rels/rel_symbolic_1_1.cvc @@ -0,0 +1,20 @@ +% 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/rels/rel_symbolic_2_1.cvc b/test/regress/regress0/rels/rel_symbolic_2_1.cvc new file mode 100644 index 000000000..082604dc2 --- /dev/null +++ b/test/regress/regress0/rels/rel_symbolic_2_1.cvc @@ -0,0 +1,21 @@ +% 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/rels/rel_symbolic_3_1.cvc b/test/regress/regress0/rels/rel_symbolic_3_1.cvc new file mode 100644 index 000000000..da0906dd2 --- /dev/null +++ b/test/regress/regress0/rels/rel_symbolic_3_1.cvc @@ -0,0 +1,21 @@ +% EXPECT: sat +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/rels/rel_tc_10_1.cvc b/test/regress/regress0/rels/rel_tc_10_1.cvc new file mode 100644 index 000000000..67c444070 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_10_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT a = c; +ASSERT a = d; +ASSERT (1, c) IS_IN x; +ASSERT (2, d) IS_IN x; +ASSERT (a, 5) IS_IN y; +ASSERT y = (TCLOSURE x); +ASSERT ((2, 5) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_11.cvc b/test/regress/regress0/rels/rel_tc_11.cvc new file mode 100644 index 000000000..7edeb0efb --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_11.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +IntTup: TYPE = [INT, INT, INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntTup; +ASSERT (2, 3) IS_IN x; +ASSERT (5, 3) IS_IN x; +ASSERT (3, 9) IS_IN x; +ASSERT z = (x PRODUCT y); +ASSERT (1, 2, 3, 4) IS_IN z; +ASSERT NOT ((5, 9) IS_IN x); +ASSERT (3, 8) IS_IN y; +ASSERT y = (TCLOSURE x); +ASSERT NOT ((1, 2) IS_IN y); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_2_1.cvc b/test/regress/regress0/rels/rel_tc_2_1.cvc new file mode 100644 index 000000000..d5d42eaad --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_2_1.cvc @@ -0,0 +1,28 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + e: INT; + +a : IntPair; +ASSERT a = (1, e); + +d : IntPair; +ASSERT d = (e,5); + +ASSERT a IS_IN x; +ASSERT d IS_IN x; +ASSERT NOT ((1,1) IS_IN x); +ASSERT NOT ((1,2) IS_IN x); +ASSERT NOT ((1,3) IS_IN x); +ASSERT NOT ((1,4) IS_IN x); +ASSERT NOT ((1,5) IS_IN x); +ASSERT NOT ((1,6) IS_IN x); +ASSERT NOT ((1,7) IS_IN x); + +ASSERT y = TCLOSURE(x); + +ASSERT (1, 5) IS_IN y; + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_3.cvc b/test/regress/regress0/rels/rel_tc_3.cvc new file mode 100644 index 000000000..39564c4cf --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_3.cvc @@ -0,0 +1,22 @@ +% 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/rels/rel_tc_3_1.cvc b/test/regress/regress0/rels/rel_tc_3_1.cvc new file mode 100644 index 000000000..7f5535656 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_3_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT (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/rels/rel_tc_4.cvc b/test/regress/regress0/rels/rel_tc_4.cvc new file mode 100644 index 000000000..decd38fe1 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_4.cvc @@ -0,0 +1,19 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +a: INT; +b:INT; +c:INT; +d:INT; +ASSERT (1, a) IS_IN x; +ASSERT (1, c) IS_IN x; +ASSERT (1, d) IS_IN x; +ASSERT (b, 1) IS_IN x; +ASSERT (b = d); +ASSERT (2,b) IS_IN ((x JOIN x) JOIN x); +ASSERT NOT (2, 1) IS_IN (TCLOSURE x); + + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_4_1.cvc b/test/regress/regress0/rels/rel_tc_4_1.cvc new file mode 100644 index 000000000..8ee75f7e9 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_4_1.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +ASSERT y = ((TCLOSURE x) JOIN x); +ASSERT NOT (y = TCLOSURE x); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_5_1.cvc b/test/regress/regress0/rels/rel_tc_5_1.cvc new file mode 100644 index 000000000..fd9caeade --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_5_1.cvc @@ -0,0 +1,9 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = (TCLOSURE x); +ASSERT NOT ( y = ((x JOIN x) JOIN x)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_6.cvc b/test/regress/regress0/rels/rel_tc_6.cvc new file mode 100644 index 000000000..4570c5a8d --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_6.cvc @@ -0,0 +1,9 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = (TCLOSURE x); +ASSERT NOT (((x JOIN x) JOIN x) <= y); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_7.cvc b/test/regress/regress0/rels/rel_tc_7.cvc new file mode 100644 index 000000000..15c0510a6 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_7.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +ASSERT y = ((TCLOSURE x) JOIN x); +ASSERT (1,2) IS_IN ((x JOIN x) JOIN x); +ASSERT NOT (y <= TCLOSURE x); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_8.cvc b/test/regress/regress0/rels/rel_tc_8.cvc new file mode 100644 index 000000000..9f5879c6d --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_8.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +ASSERT (2, 2) IS_IN (TCLOSURE x); +ASSERT x = {}::SET OF IntPair; + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tc_9_1.cvc b/test/regress/regress0/rels/rel_tc_9_1.cvc new file mode 100644 index 000000000..f884349b1 --- /dev/null +++ b/test/regress/regress0/rels/rel_tc_9_1.cvc @@ -0,0 +1,23 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +w : SET OF IntPair; + +ASSERT z = (TCLOSURE x); +ASSERT w = (x JOIN y); +ASSERT (2, 2) IS_IN z; +ASSERT (0,3) IS_IN y; +ASSERT (-1,3) IS_IN y; +ASSERT (1,3) IS_IN y; +ASSERT (-2,3) IS_IN y; +ASSERT (2,3) IS_IN y; +ASSERT (3,3) IS_IN y; +ASSERT (4,3) IS_IN y; +ASSERT (5,3) IS_IN y; +ASSERT NOT (2, 3) IS_IN (x JOIN y); +ASSERT NOT (2,1) IS_IN x; + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_tp_2.cvc b/test/regress/regress0/rels/rel_tp_2.cvc new file mode 100644 index 000000000..441e79c45 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_2.cvc @@ -0,0 +1,10 @@ +% 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/rels/rel_tp_3_1.cvc b/test/regress/regress0/rels/rel_tp_3_1.cvc new file mode 100644 index 000000000..46806b432 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_3_1.cvc @@ -0,0 +1,14 @@ +% EXPECT: sat +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 x = z; +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/rels/rel_tp_join_0.cvc b/test/regress/regress0/rels/rel_tp_join_0.cvc new file mode 100644 index 000000000..a03f0e3fd --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_0.cvc @@ -0,0 +1,32 @@ +% 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/rels/rel_tp_join_1.cvc b/test/regress/regress0/rels/rel_tp_join_1.cvc new file mode 100644 index 000000000..60b6edf58 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_1.cvc @@ -0,0 +1,32 @@ +% 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/rels/rel_tp_join_2.cvc b/test/regress/regress0/rels/rel_tp_join_2.cvc new file mode 100644 index 000000000..cc851f622 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_2.cvc @@ -0,0 +1,19 @@ +% 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/rels/rel_tp_join_2_1.cvc b/test/regress/regress0/rels/rel_tp_join_2_1.cvc new file mode 100644 index 000000000..acf3dbccf --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_2_1.cvc @@ -0,0 +1,19 @@ +% EXPECT: sat +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/rels/rel_tp_join_3.cvc b/test/regress/regress0/rels/rel_tp_join_3.cvc new file mode 100644 index 000000000..25277f43a --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_3.cvc @@ -0,0 +1,28 @@ +% 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/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc new file mode 100644 index 000000000..54e16dd51 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_eq_0.cvc @@ -0,0 +1,28 @@ +% 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/rels/rel_tp_join_int_0.cvc b/test/regress/regress0/rels/rel_tp_join_int_0.cvc new file mode 100644 index 000000000..8d149a48d --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_int_0.cvc @@ -0,0 +1,26 @@ +% 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/rels/rel_tp_join_pro_0.cvc b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc new file mode 100644 index 000000000..b05026bc9 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_pro_0.cvc @@ -0,0 +1,21 @@ +% 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/rels/rel_tp_join_var_0.cvc b/test/regress/regress0/rels/rel_tp_join_var_0.cvc new file mode 100644 index 000000000..aacf6c054 --- /dev/null +++ b/test/regress/regress0/rels/rel_tp_join_var_0.cvc @@ -0,0 +1,28 @@ +% 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/rels/rel_transpose_0.cvc b/test/regress/regress0/rels/rel_transpose_0.cvc new file mode 100644 index 000000000..49fb87569 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_0.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +a: INT; +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/rels/rel_transpose_1.cvc b/test/regress/regress0/rels/rel_transpose_1.cvc new file mode 100644 index 000000000..bdcf31bb8 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_1.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntTup: TYPE = [INT, INT, INT]; +x : SET OF IntTup; +y : SET OF IntTup; +z : IntTup; +ASSERT z = (1,2,3); +zt : IntTup; +ASSERT zt = (3,2,1); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE x)); +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_transpose_1_1.cvc b/test/regress/regress0/rels/rel_transpose_1_1.cvc new file mode 100644 index 000000000..fa6ee5069 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_1_1.cvc @@ -0,0 +1,14 @@ +% 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/rels/rel_transpose_3.cvc b/test/regress/regress0/rels/rel_transpose_3.cvc new file mode 100644 index 000000000..5dfe3b031 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_3.cvc @@ -0,0 +1,15 @@ +% 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 (x = y); +ASSERT z IS_IN x; +ASSERT NOT (zt IS_IN (TRANSPOSE y)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/rel_transpose_4.cvc b/test/regress/regress0/rels/rel_transpose_4.cvc new file mode 100644 index 000000000..b260147c8 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_4.cvc @@ -0,0 +1,13 @@ +% 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/rels/rel_transpose_5.cvc b/test/regress/regress0/rels/rel_transpose_5.cvc new file mode 100644 index 000000000..203e8b3d2 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_5.cvc @@ -0,0 +1,22 @@ +% 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/rels/rel_transpose_6.cvc b/test/regress/regress0/rels/rel_transpose_6.cvc new file mode 100644 index 000000000..a2e8bcf10 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_6.cvc @@ -0,0 +1,24 @@ +% 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/rels/rel_transpose_7.cvc b/test/regress/regress0/rels/rel_transpose_7.cvc new file mode 100644 index 000000000..bcc3babc8 --- /dev/null +++ b/test/regress/regress0/rels/rel_transpose_7.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; + +ASSERT x = y; +ASSERT NOT (TRANSPOSE(x) = TRANSPOSE(y)); + +CHECKSAT; diff --git a/test/regress/regress0/rels/set-strat.cvc b/test/regress/regress0/rels/set-strat.cvc new file mode 100644 index 000000000..0dee0e84d --- /dev/null +++ b/test/regress/regress0/rels/set-strat.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/strat.cvc b/test/regress/regress0/rels/strat.cvc new file mode 100644 index 000000000..b91ddbbe8 --- /dev/null +++ b/test/regress/regress0/rels/strat.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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/regress0/rels/strat_0_1.cvc b/test/regress/regress0/rels/strat_0_1.cvc new file mode 100644 index 000000000..b91ddbbe8 --- /dev/null +++ b/test/regress/regress0/rels/strat_0_1.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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; |