From e116c00719a7574064c09da4abb10b3297415c90 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 22 Sep 2021 13:38:46 -0700 Subject: Remove CVC language support (#7219) This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2. --- test/regress/regress1/rels/addr_book_1.cvc.smt2 | 38 +++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test/regress/regress1/rels/addr_book_1.cvc.smt2 (limited to 'test/regress/regress1/rels/addr_book_1.cvc.smt2') diff --git a/test/regress/regress1/rels/addr_book_1.cvc.smt2 b/test/regress/regress1/rels/addr_book_1.cvc.smt2 new file mode 100644 index 000000000..7a6ac7d5b --- /dev/null +++ b/test/regress/regress1/rels/addr_book_1.cvc.smt2 @@ -0,0 +1,38 @@ +; 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 m () Atom) +(declare-fun m_tup () (Tuple Atom)) +(assert (= m_tup (mkTuple m))) +(assert (member m_tup Name)) +(declare-fun t () Atom) +(declare-fun t_tup () (Tuple Atom)) +(assert (= t_tup (mkTuple t))) +(assert (member t_tup Target)) +(assert (= (join (singleton m_tup) (join (singleton b1_tup) addr)) (as emptyset (Set (Tuple Atom))))) +(assert (= (join (singleton b2_tup) addr) (union (join (singleton b1_tup) addr) (singleton (mkTuple m t))))) +(assert (= (join (singleton b3_tup) addr) (setminus (join (singleton b2_tup) addr) (singleton (mkTuple m t))))) +(assert (not (= (join (singleton b1_tup) addr) (join (singleton b3_tup) addr)))) +(check-sat) -- cgit v1.2.3