From e116c00719a7574064c09da4abb10b3297415c90 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
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/sets/arjun-set-univ.cvc       |  8 --------
 test/regress/regress1/sets/arjun-set-univ.cvc.smt2  | 19 +++++++++++++++++++
 test/regress/regress1/sets/choose.cvc               | 11 -----------
 test/regress/regress1/sets/choose.cvc.smt2          | 10 ++++++++++
 test/regress/regress1/sets/sets-tuple-poly.cvc      | 18 ------------------
 test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 | 13 +++++++++++++
 6 files changed, 42 insertions(+), 37 deletions(-)
 delete mode 100644 test/regress/regress1/sets/arjun-set-univ.cvc
 create mode 100644 test/regress/regress1/sets/arjun-set-univ.cvc.smt2
 delete mode 100644 test/regress/regress1/sets/choose.cvc
 create mode 100644 test/regress/regress1/sets/choose.cvc.smt2
 delete mode 100644 test/regress/regress1/sets/sets-tuple-poly.cvc
 create mode 100644 test/regress/regress1/sets/sets-tuple-poly.cvc.smt2

(limited to 'test/regress/regress1/sets')

diff --git a/test/regress/regress1/sets/arjun-set-univ.cvc b/test/regress/regress1/sets/arjun-set-univ.cvc
deleted file mode 100644
index 3c35a62a5..000000000
--- a/test/regress/regress1/sets/arjun-set-univ.cvc
+++ /dev/null
@@ -1,8 +0,0 @@
-% EXPECT: Extended set operators are not supported in default mode, try --sets-ext.
-% EXIT: 1
-OPTION "produce-models" true;
-x,y,z : SET OF BOOLEAN;
-ASSERT x = {TRUE};
-ASSERT y = {FALSE};
-CHECKSAT z = ~ y;
-COUNTERMODEL;
diff --git a/test/regress/regress1/sets/arjun-set-univ.cvc.smt2 b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2
new file mode 100644
index 000000000..b76b48f2d
--- /dev/null
+++ b/test/regress/regress1/sets/arjun-set-univ.cvc.smt2
@@ -0,0 +1,19 @@
+; EXIT: 1
+; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.")
+(set-logic ALL)
+(set-option :incremental true)
+(set-option :produce-models true)
+(declare-fun x () (Set Bool))
+(declare-fun y () (Set Bool))
+(declare-fun z () (Set Bool))
+(assert (= x (singleton true)))
+(assert (= y (singleton false)))
+(push 1)
+
+(assert (= z (complement y)))
+
+(check-sat)
+
+(pop 1)
+
+(get-model)
diff --git a/test/regress/regress1/sets/choose.cvc b/test/regress/regress1/sets/choose.cvc
deleted file mode 100644
index a8c5b2495..000000000
--- a/test/regress/regress1/sets/choose.cvc
+++ /dev/null
@@ -1,11 +0,0 @@
-% COMMAND-LINE:
-% EXPECT: sat
-
-A : SET OF INT;
-a : INT;
-
-ASSERT NOT (A = {} :: SET OF INT);
-ASSERT CHOOSE (A) = 10;
-ASSERT CHOOSE (A) = a;
-
-CHECKSAT;
diff --git a/test/regress/regress1/sets/choose.cvc.smt2 b/test/regress/regress1/sets/choose.cvc.smt2
new file mode 100644
index 000000000..8c3be2f99
--- /dev/null
+++ b/test/regress/regress1/sets/choose.cvc.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE:
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun A () (Set Int))
+(declare-fun a () Int)
+(assert (not (= A (as emptyset (Set Int)))))
+(assert (= (choose A) 10))
+(assert (= (choose A) a))
+(check-sat)
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc b/test/regress/regress1/sets/sets-tuple-poly.cvc
deleted file mode 100644
index d286e46e4..000000000
--- a/test/regress/regress1/sets/sets-tuple-poly.cvc
+++ /dev/null
@@ -1,18 +0,0 @@
-% COMMAND-LINE:
-% EXPECT: sat
-OPTION "sets-ext";
-OPTION "logic" "ALL";
-
-a : SET OF [REAL, INT];
-b : SET OF [INT, REAL];
-
-x : [ REAL, REAL ];
-
-ASSERT NOT x = (0.0,0.0);
-
-ASSERT (x.0, FLOOR(x.1)) IS_IN a;
-ASSERT (FLOOR(x.0), x.1) IS_IN b;
-
-ASSERT NOT x.0 = x.1;
-
-CHECKSAT;
diff --git a/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2 b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2
new file mode 100644
index 000000000..d15aa3030
--- /dev/null
+++ b/test/regress/regress1/sets/sets-tuple-poly.cvc.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE:
+; EXPECT: sat
+(set-option :incremental false)
+(set-option :sets-ext true)
+(set-logic ALL)
+(declare-fun a () (Set (Tuple Real Int)))
+(declare-fun b () (Set (Tuple Int Real)))
+(declare-fun x () (Tuple Real Real))
+(assert (let ((_let_1 0.0)) (not (= x (mkTuple _let_1 _let_1)))))
+(assert (member (mkTuple ((_ tupSel 0) x) (to_int ((_ tupSel 1) x))) a))
+(assert (member (mkTuple (to_int ((_ tupSel 0) x)) ((_ tupSel 1) x)) b))
+(assert (not (= ((_ tupSel 0) x) ((_ tupSel 1) x))))
+(check-sat)
-- 
cgit v1.2.3