diff options
Diffstat (limited to 'test/regress/regress1/rels/joinImg_0_1.cvc')
-rw-r--r-- | test/regress/regress1/rels/joinImg_0_1.cvc | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/joinImg_0_1.cvc b/test/regress/regress1/rels/joinImg_0_1.cvc new file mode 100644 index 000000000..4e69394bd --- /dev/null +++ b/test/regress/regress1/rels/joinImg_0_1.cvc @@ -0,0 +1,36 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; + +t : SET OF [INT]; +u : 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); +b: INT; + +ASSERT (1, 7) IS_IN x; +ASSERT z IS_IN x; + +ASSERT (7, 5) IS_IN y; + +ASSERT t = (x JOIN_IMAGE 2); + +ASSERT TUPLE(3) IS_IN (x JOIN_IMAGE 2); + +ASSERT u = (x JOIN_IMAGE 1); + +ASSERT TUPLE(4) IS_IN (x JOIN_IMAGE 2); + +ASSERT TUPLE(b) IS_IN (x JOIN_IMAGE 1); +CHECKSAT; |