Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.

1 files changed, 0 insertions, 65 deletions

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 13beedd63..bfaf8bda0 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -304,71 +304,6 @@ public:
   }
 };/* class Cvc4ParserTest */
 
-class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
-  typedef ParserBlack super;
-
-public:
-  Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
-
-  void setUp() override { super::setUp(); }
-
-  void tearDown() override { super::tearDown(); }
-
-  void testGoodSmt1Inputs() {
-    tryGoodInput(""); // empty string is OK
-    tryGoodInput("(benchmark foo :assumption true)");
-    tryGoodInput("(benchmark bar :formula true)");
-    tryGoodInput("(benchmark qux :formula false)");
-    tryGoodInput("(benchmark baz :extrapreds ( (a) (b) ) )");
-    tryGoodInput("(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))");
-    tryGoodInput("(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) )  :formula (= (f x) x))");
-    tryGoodInput("(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))");
-    tryGoodInput(";; nothing but a comment");
-    tryGoodInput("; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)");
-  }
-
-  void testBadSmt1Inputs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
-    tryBadInput("(benchmark foo)"); // empty benchmark is not OK
-    tryBadInput("(benchmark bar :assumption)"); // no args
-    tryBadInput("(benchmark bar :formula)");
-    tryBadInput("(benchmark baz :extrapreds ( (a) (a) ) )"); // double decl
-    tryBadInput("(benchmark zub :extrasorts (a) :extrapreds (p a))"); // (p a) needs parens
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-
-  void testGoodSmt1Exprs() {
-    tryGoodExpr("(and a b)");
-    tryGoodExpr("(or (and a b) c)");
-    tryGoodExpr("(implies (and (implies a b) a) b)");
-    tryGoodExpr("(and (iff a b) (not a))");
-    tryGoodExpr("(iff (xor a b) (and (or a b) (not (and a b))))");
-    tryGoodExpr("(ite a (f x) y)");
-    tryGoodExpr("(if_then_else a (f x) y)");
-    tryGoodExpr("1");
-    tryGoodExpr("0");
-    tryGoodExpr("1.5");
-  }
-
-  void testBadSmt1Exprs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
-    tryBadExpr("(and)"); // wrong arity
-    tryBadExpr("(and a b"); // no closing paren
-    tryBadExpr("(a and b)"); // infix
-    tryBadExpr("(OR (AND a b) c)"); // wrong case
-    tryBadExpr("(a IMPLIES b)"); // infix AND wrong case
-    tryBadExpr("(not a b)"); // wrong arity
-    tryBadExpr("not a"); // needs parens
-    tryBadExpr("(ite a x)"); // wrong arity
-    tryBadExpr("(a b)"); // using non-function as function
-    tryBadExpr(".5"); // rational constants must have integer prefix
-    tryBadExpr("1."); // rational constants must have fractional suffix
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-};/* class Smt1ParserTest */
-
 class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;