diff options
Diffstat (limited to 'test/regress/regress1/rels/rel_complex_5.cvc')
-rw-r--r-- | test/regress/regress1/rels/rel_complex_5.cvc | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/rel_complex_5.cvc b/test/regress/regress1/rels/rel_complex_5.cvc new file mode 100644 index 000000000..d64817187 --- /dev/null +++ b/test/regress/regress1/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; + + + + + + + + + + + + + + |