diff options
Diffstat (limited to 'test/regress/regress0/rels/addr_book_0.cvc.smt2')
| -rw-r--r-- | test/regress/regress0/rels/addr_book_0.cvc.smt2 | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 new file mode 100644 index 000000000..a27be5b4b --- /dev/null +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -0,0 +1,41 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(declare-sort Atom 0) + + + +(declare-fun Target () (Set (Tuple Atom))) +(declare-fun Name () (Set (Tuple Atom))) +(declare-fun Addr () (Set (Tuple Atom))) +(declare-fun Book () (Set (Tuple Atom))) +(declare-fun names () (Set (Tuple Atom Atom))) +(declare-fun addr () (Set (Tuple Atom Atom Atom))) +(declare-fun b1 () Atom) +(declare-fun b1_tup () (Tuple Atom)) +(assert (= b1_tup (mkTuple b1))) +(assert (member b1_tup Book)) +(declare-fun b2 () Atom) +(declare-fun b2_tup () (Tuple Atom)) +(assert (= b2_tup (mkTuple b2))) +(assert (member b2_tup Book)) +(declare-fun b3 () Atom) +(declare-fun b3_tup () (Tuple Atom)) +(assert (= b3_tup (mkTuple b3))) +(assert (member b3_tup Book)) +(declare-fun n () Atom) +(declare-fun n_tup () (Tuple Atom)) +(assert (= n_tup (mkTuple n))) +(assert (member n_tup Name)) +(declare-fun t () Atom) +(declare-fun t_tup () (Tuple Atom)) +(assert (= t_tup (mkTuple t))) +(assert (member t_tup Target)) +(assert (subset (join (join Book addr) Target) Name)) +(assert (subset (join Book names) Name)) +(assert (= (intersection Name Addr) (as emptyset (Set (Tuple Atom))))) +(assert (= (join (singleton n_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) +(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b2_tup) addr)) (union (join _let_1 (join (singleton b1_tup) addr)) (singleton t_tup))))) +(assert (let ((_let_1 (singleton n_tup))) (= (join _let_1 (join (singleton b3_tup) addr)) (setminus (join _let_1 (join (singleton b2_tup) addr)) (singleton t_tup))))) +(assert (let ((_let_1 (singleton n_tup))) (not (= (join _let_1 (join (singleton b1_tup) addr)) (join _let_1 (join (singleton b3_tup) addr)))))) +(check-sat) |