diff options
Diffstat (limited to 'test/regress/regress0/rels/relations-ops.smt2')
| -rw-r--r-- | test/regress/regress0/rels/relations-ops.smt2 | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/relations-ops.smt2 b/test/regress/regress0/rels/relations-ops.smt2 new file mode 100644 index 000000000..abb7faf10 --- /dev/null +++ b/test/regress/regress0/rels/relations-ops.smt2 @@ -0,0 +1,23 @@ +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun r1 () (Set (Tuple String Int))) +(declare-fun r2 () (Set (Tuple Int String))) +(declare-fun r () (Set (Tuple String String))) +(declare-fun s () (Set (Tuple String String))) +(declare-fun t () (Set (Tuple String Int Int String))) +(declare-fun lt1 () (Set (Tuple Int Int))) +(declare-fun lt2 () (Set (Tuple Int Int))) +(declare-fun i () Int) + +(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4))))) +(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17"))))) +(assert (= r (join r1 r2))) +(assert (= s (transpose r))) +(assert (= t (product r1 r2))) +(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5))))) +(assert (= lt2 (tclosure lt1))) +(assert (= i (card t))) + +(check-sat) |