diff options
author | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
---|---|---|
committer | Paul Meng <baolmeng@gmail.com> | 2017-04-20 14:04:24 -0500 |
commit | 7152d6136fc8bd4701d9440ba3eee6bb7bf3a16c (patch) | |
tree | 9012cc085fcde111d5a0609441415cdbb1a7b460 /test/regress/regress0/rels/iden_0.cvc | |
parent | c110fa8d07b5650c671b99797c17822e757bc52f (diff) |
Support for relational operators identity and join image
Diffstat (limited to 'test/regress/regress0/rels/iden_0.cvc')
-rw-r--r-- | test/regress/regress0/rels/iden_0.cvc | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/iden_0.cvc b/test/regress/regress0/rels/iden_0.cvc new file mode 100644 index 000000000..4c2693084 --- /dev/null +++ b/test/regress/regress0/rels/iden_0.cvc @@ -0,0 +1,28 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom: TYPE; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +id : SET OF IntPair; + +t : 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); + +ASSERT TUPLE(1) IS_IN t; +ASSERT TUPLE(2) IS_IN t; +ASSERT z IS_IN x; +ASSERT zt IS_IN x; +ASSERT v IS_IN x; +ASSERT a IS_IN x; +ASSERT id = IDEN(t); +ASSERT NOT ((1, 1) IS_IN (id & x)); + +CHECKSAT; |