diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-03-04 11:27:02 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-03-04 11:27:02 -0600 |
commit | 0231618679e6f2e4ae6247015fc5eb0f2f35f9fe (patch) | |
tree | fc410a58c66151968e6c52658d581525c6f7d731 /test/regress/regress0/sets | |
parent | 31ab3e21f285b0b6a3a8de7ab352c0c6276b6695 (diff) |
refactored the code
- send out facts as lemmas
- fixed the non-termination problem caused by sending facts as lemmas
- unfolded symbolic tuples by adding equality lemmas
Diffstat (limited to 'test/regress/regress0/sets')
7 files changed, 110 insertions, 6 deletions
diff --git a/test/regress/regress0/sets/rels/rel_join_0_1.cvc b/test/regress/regress0/sets/rels/rel_join_0_1.cvc index 70e35164a..a7fa7efb9 100644 --- a/test/regress/regress0/sets/rels/rel_join_0_1.cvc +++ b/test/regress/regress0/sets/rels/rel_join_0_1.cvc @@ -15,6 +15,7 @@ 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; diff --git a/test/regress/regress0/sets/rels/rel_symbolic_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1.cvc new file mode 100644 index 000000000..08ed32411 --- /dev/null +++ b/test/regress/regress0/sets/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/sets/rels/rel_symbolic_1_1.cvc b/test/regress/regress0/sets/rels/rel_symbolic_1_1.cvc new file mode 100644 index 000000000..df2d7f412 --- /dev/null +++ b/test/regress/regress0/sets/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/sets/rels/rel_tp_join_1.cvc b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc index dca0a3bfa..60b6edf58 100644 --- a/test/regress/regress0/sets/rels/rel_tp_join_1.cvc +++ b/test/regress/regress0/sets/rels/rel_tp_join_1.cvc @@ -6,12 +6,20 @@ y : SET OF IntPair; z : SET OF IntPair; r : SET OF IntPair; -ASSERT (1, 7) IS_IN x; -ASSERT (2, 3) IS_IN x; +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 (7, 3) IS_IN y; -ASSERT (4, 7) IS_IN y; +ASSERT d IS_IN y; +ASSERT e IS_IN y; ASSERT (3, 4) IS_IN z; diff --git a/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc b/test/regress/regress0/sets/rels/rel_tp_join_eq_0.cvc new file mode 100644 index 000000000..54e16dd51 --- /dev/null +++ b/test/regress/regress0/sets/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/sets/rels/rel_tp_join_int.cvc b/test/regress/regress0/sets/rels/rel_tp_join_int.cvc new file mode 100644 index 000000000..8d149a48d --- /dev/null +++ b/test/regress/regress0/sets/rels/rel_tp_join_int.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/sets/rels/rel_tp_join_var.cvc b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc index c7757bd3e..aacf6c054 100644 --- a/test/regress/regress0/sets/rels/rel_tp_join_var.cvc +++ b/test/regress/regress0/sets/rels/rel_tp_join_var.cvc @@ -13,8 +13,8 @@ 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; +ASSERT (1, t) IS_IN x; +ASSERT (u, 3) IS_IN y; a : IntPair; ASSERT a = (1,3); |