Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

1 files changed, 38 insertions, 0 deletions

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)