diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-04-20 17:08:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-04-20 17:08:08 -0500 |
| commit | 8a0d2b0577e174d2078026129dd01ea46f7f984a (patch) | |
| tree | 5ddcdb9526db5e1694aea174588663dd92a31a7c /test/regress/regress0/rels/joinImg_2_1.cvc | |
| parent | 96f66b5c2bb1feaf594fc1facbd2fb44e0f71cb0 (diff) | |
| parent | 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c (diff) | |
Merge pull request #149 from PaulMeng/master
Support for relational operators identity and join image
Diffstat (limited to 'test/regress/regress0/rels/joinImg_2_1.cvc')
| -rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc new file mode 100644 index 000000000..b38bfab06 --- /dev/null +++ b/test/regress/regress0/rels/joinImg_2_1.cvc @@ -0,0 +1,24 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +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;
\ No newline at end of file |