Remove CVC language support (#7219)

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

10 files changed, 92 insertions, 91 deletions

diff --git a/test/regress/regress0/push-pop/bug233.cvc b/test/regress/regress0/push-pop/bug233.cvc
deleted file mode 100644
index 1a6049329..000000000
--- a/test/regress/regress0/push-pop/bug233.cvc
+++ /dev/null
@@ -1,11 +0,0 @@
-% Tests the invariants for multiple queries.
-% COMMAND-LINE: --incremental
-
-a, b: BOOLEAN;
-
-% EXPECT: entailed
-QUERY (a AND b) OR NOT (a AND b);
-
-% EXPECT: not_entailed
-QUERY (a OR b);
-
diff --git a/test/regress/regress0/push-pop/bug233.cvc.smt2 b/test/regress/regress0/push-pop/bug233.cvc.smt2
new file mode 100644
index 000000000..422f8d5ca
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug233.cvc.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(check-sat-assuming ( (not (let ((_let_1 (and a b))) (or _let_1 (not _let_1)))) ))
+(check-sat-assuming ( (not (or a b)) ))
diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc b/test/regress/regress0/push-pop/incremental-subst-bug.cvc
deleted file mode 100644
index 657e74486..000000000
--- a/test/regress/regress0/push-pop/incremental-subst-bug.cvc
+++ /dev/null
@@ -1,21 +0,0 @@
-% COMMAND-LINE: --incremental
-U : TYPE;
-x, y : U;
-% EXPECT: not_entailed
-QUERY x = y;
-ASSERT x = y;
-% EXPECT: entailed
-QUERY x = y;
-PUSH;
-z : U;
-% EXPECT: entailed
-QUERY x = y;
-% EXPECT: not_entailed
-QUERY x = z;
-% EXPECT: not_entailed
-QUERY z = x;
-% EXPECT: not_entailed
-QUERY z /= x;
-POP;
-% EXPECT: not_entailed
-QUERY z /= x;
diff --git a/test/regress/regress0/push-pop/incremental-subst-bug.cvc.smt2 b/test/regress/regress0/push-pop/incremental-subst-bug.cvc.smt2
new file mode 100644
index 000000000..dc94e8f94
--- /dev/null
+++ b/test/regress/regress0/push-pop/incremental-subst-bug.cvc.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort U 0)
+(declare-fun x () U)
+(declare-fun y () U)
+(check-sat-assuming ( (not (= x y)) ))
+(assert (= x y))
+(check-sat-assuming ( (not (= x y)) ))
+(declare-fun z () U)
+(push 1)
+(check-sat-assuming ( (not (= x y)) ))
+(check-sat-assuming ( (not (= x z)) ))
+(check-sat-assuming ( (not (= z x)) ))
+(check-sat-assuming ( (= z x) ))
+(pop 1)
+(check-sat-assuming ( (= z x) ))
diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc
deleted file mode 100644
index 78d7b9f2c..000000000
--- a/test/regress/regress0/push-pop/test.00.cvc
+++ /dev/null
@@ -1,11 +0,0 @@
-% COMMAND-LINE: --incremental
-x: BOOLEAN;
-
-PUSH;
-ASSERT x;
-% EXPECT: sat
-CHECKSAT;
-POP;
-ASSERT (NOT x);
-% EXPECT: sat
-CHECKSAT;
diff --git a/test/regress/regress0/push-pop/test.00.cvc.smt2 b/test/regress/regress0/push-pop/test.00.cvc.smt2
new file mode 100644
index 000000000..2a1de615e
--- /dev/null
+++ b/test/regress/regress0/push-pop/test.00.cvc.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Bool)
+(push 1)
+(assert x)
+(check-sat)
+(pop 1)
+(assert (not x))
+(check-sat)
diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
deleted file mode 100644
index 2bb5877f5..000000000
--- a/test/regress/regress0/push-pop/test.01.cvc
+++ /dev/null
@@ -1,19 +0,0 @@
-% COMMAND-LINE: --incremental
-
-x, y: BOOLEAN;
-
-ASSERT (x OR y);
-% EXPECT: sat
-CHECKSAT;
-PUSH;
-ASSERT (NOT x);
-% EXPECT: sat
-CHECKSAT;
-POP;
-PUSH;
-ASSERT (NOT y);
-% EXPECT: sat
-CHECKSAT;
-POP;
-% EXPECT: sat
-CHECKSAT;
diff --git a/test/regress/regress0/push-pop/test.01.cvc.smt2 b/test/regress/regress0/push-pop/test.01.cvc.smt2
new file mode 100644
index 000000000..23342e334
--- /dev/null
+++ b/test/regress/regress0/push-pop/test.01.cvc.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (or x y))
+(check-sat)
+(push 1)
+(assert (not x))
+(check-sat)
+(pop 1)
+(push 1)
+(assert (not y))
+(check-sat)
+(pop 1)
+(check-sat)
diff --git a/test/regress/regress0/push-pop/units.cvc b/test/regress/regress0/push-pop/units.cvc
deleted file mode 100644
index 3550174d8..000000000
--- a/test/regress/regress0/push-pop/units.cvc
+++ /dev/null
@@ -1,29 +0,0 @@
-% COMMAND-LINE: --incremental
-x, y: BOOLEAN;
-ASSERT x OR y;
-% EXPECT: sat
-CHECKSAT;
-PUSH;
-  ASSERT NOT x;
-% EXPECT: sat
-  CHECKSAT;
-  PUSH;
-    ASSERT NOT y;
-% EXPECT: unsat
-    CHECKSAT;
-  POP;
-% EXPECT: sat
-  CHECKSAT;
-POP;
-% EXPECT: sat
-CHECKSAT;
-PUSH 2;
-ASSERT x;
-ASSERT NOT x;
-% EXPECT: unsat
-CHECKSAT;
-POP 2;
-% EXPECT: sat
-CHECKSAT;
-
-
diff --git a/test/regress/regress0/push-pop/units.cvc.smt2 b/test/regress/regress0/push-pop/units.cvc.smt2
new file mode 100644
index 000000000..7d1feadf4
--- /dev/null
+++ b/test/regress/regress0/push-pop/units.cvc.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () Bool)
+(declare-fun y () Bool)
+(assert (or x y))
+(check-sat)
+(push 1)
+(assert (not x))
+(check-sat)
+(push 1)
+(assert (not y))
+(check-sat)
+(pop 1)
+(check-sat)
+(pop 1)
+(check-sat)
+(push 1)
+(push 1)
+(assert x)
+(assert (not x))
+(check-sat)
+(pop 1)
+(pop 1)
+(check-sat)