diff options
author | Arjun Viswanathan <arjun-viswanathan@uiowa.edu> | 2017-12-27 21:43:35 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-27 21:43:35 -0600 |
commit | 2731897b5f9ed46c66e3bdf20cde47ef43923a9c (patch) | |
tree | a95d36fdeb9c6a0d5dbc41ef4dc7bafdcb6e81b3 /test/regress/regress0/rels | |
parent | 3b7f04092f55b263b1f89fa2c2517821013ff5fe (diff) |
Rel smt parser (#1446)
Diffstat (limited to 'test/regress/regress0/rels')
-rw-r--r-- | test/regress/regress0/rels/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/rels/relations-ops.smt2 | 23 |
2 files changed, 25 insertions, 1 deletions
diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index 7f772a8e1..c8fb739d0 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -113,7 +113,8 @@ TESTS = \ joinImg_1.cvc \ joinImg_2_1.cvc \ joinImg_2.cvc \ - card_transpose.cvc + card_transpose.cvc \ + relations-ops.smt2 # unsolved : garbage_collect.cvc 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) |