google test: parser: Migrate parser_black. (#5886)

3 files changed, 398 insertions, 413 deletions

diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 4202ea0c9..7e413e707 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -11,5 +11,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_cxx_unit_test_black(parser_black parser)
+cvc4_add_unit_test_black(parser_black parser)
 cvc4_add_cxx_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
new file mode 100644
index 000000000..9f17e78dd
--- /dev/null
+++ b/test/unit/parser/parser_black.cpp
@@ -0,0 +1,397 @@
+/*********************                                                        */
+/*! \file parser_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Christopher L. Conway, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::parser::Parser for CVC and SMT-LIBv2
+ ** inputs.
+ **
+ ** Black box testing of CVC4::parser::Parser for CVC and SMT-LIbv2 inputs.
+ **/
+
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+#include "base/output.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/symbol_manager.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/options.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "parser/smt2/smt2.h"
+#include "smt/command.h"
+#include "test.h"
+
+namespace CVC4 {
+
+using namespace parser;
+using namespace language::input;
+
+namespace test {
+
+class TestParserBlackParser : public TestInternal
+{
+ protected:
+  TestParserBlackParser(InputLanguage lang) : d_lang(lang) {}
+
+  virtual ~TestParserBlackParser() {}
+
+  void SetUp() override
+  {
+    TestInternal::SetUp();
+    d_options.set(options::parseOnly, true);
+    d_symman.reset(nullptr);
+    d_solver.reset(new CVC4::api::Solver(&d_options));
+  }
+
+  void TearDown() override
+  {
+    d_symman.reset(nullptr);
+    d_solver.reset(nullptr);
+  }
+
+  void setUp()
+  {
+    /* ensure the old symbol manager is deleted */
+    d_symman.reset(nullptr);
+    d_solver.reset(new api::Solver(&d_options));
+  }
+
+  /* Set up declaration context for expr inputs */
+  void setupContext(Parser& parser)
+  {
+    /* a, b, c: BOOLEAN */
+    parser.bindVar("a", d_solver.get()->getBooleanSort());
+    parser.bindVar("b", d_solver.get()->getBooleanSort());
+    parser.bindVar("c", d_solver.get()->getBooleanSort());
+    /* t, u, v: TYPE */
+    api::Sort t = parser.mkSort("t");
+    api::Sort u = parser.mkSort("u");
+    api::Sort v = parser.mkSort("v");
+    /* f : t->u; g: u->v; h: v->t; */
+    parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u));
+    parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v));
+    parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t));
+    /* x:t; y:u; z:v; */
+    parser.bindVar("x", t);
+    parser.bindVar("y", u);
+    parser.bindVar("z", v);
+  }
+
+  void tryGoodInput(const std::string goodInput)
+  {
+    d_symman.reset(new SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+                         .withStringInput(goodInput)
+                         .withOptions(d_options)
+                         .withInputLanguage(d_lang)
+                         .build();
+    ASSERT_FALSE(parser->done());
+    Command* cmd;
+    while ((cmd = parser->nextCommand()) != NULL)
+    {
+      Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
+      delete cmd;
+    }
+
+    ASSERT_TRUE(parser->done());
+    delete parser;
+  }
+
+  void tryBadInput(const std::string badInput, bool strictMode = false)
+  {
+    d_symman.reset(new SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+                         .withStringInput(badInput)
+                         .withOptions(d_options)
+                         .withInputLanguage(d_lang)
+                         .withStrictMode(strictMode)
+                         .build();
+    ASSERT_THROW(
+        {
+          Command* cmd;
+          while ((cmd = parser->nextCommand()) != NULL)
+          {
+            Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
+            delete cmd;
+          }
+          std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
+        },
+        ParserException);
+    delete parser;
+  }
+
+  void tryGoodExpr(const std::string goodExpr)
+  {
+    d_symman.reset(new SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+                         .withStringInput(goodExpr)
+                         .withOptions(d_options)
+                         .withInputLanguage(d_lang)
+                         .build();
+
+    if (d_lang == LANG_SMTLIB_V2)
+    {
+      /* Use QF_LIA to make multiplication ("*") available */
+      std::unique_ptr<Command> cmd(
+          static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
+    }
+
+    ASSERT_FALSE(parser->done());
+    setupContext(*parser);
+    ASSERT_FALSE(parser->done());
+    api::Term e = parser->nextExpression();
+    ASSERT_FALSE(e.isNull());
+    e = parser->nextExpression();
+    ASSERT_TRUE(parser->done());
+    ASSERT_TRUE(e.isNull());
+    delete parser;
+  }
+
+  /**
+   * NOTE: The check implemented here may fail if a bad expression
+   * expression string has a prefix that is parseable as a good
+   * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
+   * actually return the bit-vector 10 and ignore the tail of the
+   * input. It's more trouble than it's worth to check that the whole
+   * input was consumed here, so just be careful to avoid valid
+   * prefixes in tests.
+   */
+  void tryBadExpr(const std::string badExpr, bool strictMode = false)
+  {
+    d_symman.reset(new SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
+                         .withStringInput(badExpr)
+                         .withOptions(d_options)
+                         .withInputLanguage(d_lang)
+                         .withStrictMode(strictMode)
+                         .build();
+    setupContext(*parser);
+    ASSERT_FALSE(parser->done());
+    ASSERT_THROW(api::Term e = parser->nextExpression();
+                 std::cout << std::endl
+                           << "Bad expr succeeded." << std::endl
+                           << "Input: <<" << badExpr << ">>" << std::endl
+                           << "Output: <<" << e << ">>" << std::endl;
+                 , ParserException);
+    delete parser;
+  }
+
+  Options d_options;
+  InputLanguage d_lang;
+  std::unique_ptr<CVC4::api::Solver> d_solver;
+  std::unique_ptr<SymbolManager> d_symman;
+};
+
+/* -------------------------------------------------------------------------- */
+
+class TestParserBlackCvCParser : public TestParserBlackParser
+{
+ protected:
+  TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC4) {}
+};
+
+TEST_F(TestParserBlackCvCParser, good_inputs)
+{
+  tryGoodInput("");   // empty string is OK
+  tryGoodInput(";");  // no command is OK
+  tryGoodInput("ASSERT TRUE;");
+  tryGoodInput("QUERY TRUE;");
+  tryGoodInput("CHECKSAT FALSE;");
+  tryGoodInput("a, b : BOOLEAN;");
+  tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
+  tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
+  tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
+  tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];");
+  tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;");
+  tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
+  tryGoodInput(
+      "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
+  tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
+  tryGoodInput("%% nothing but a comment");
+  tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
+  tryGoodInput("a : BOOLEAN; a: BOOLEAN;");  // double decl, but compatible
+  tryGoodInput("a : INT = 5; a: INT;");      // decl after define, compatible
+  tryGoodInput(
+      "a : TYPE; a : INT;");  // ok, sort and variable symbol spaces distinct
+  tryGoodInput(
+      "a : TYPE; a : INT; b : a;");  // ok except a is both INT and sort `a'
+  tryGoodInput(
+      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null "
+      "END;");
+  tryGoodInput(
+      "DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil "
+      "END;");
+  tryGoodInput(
+      "DATATYPE trex = Foo | Bar END; DATATYPE tree = "
+      "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list "
+      "OF tree,cdr:BITVECTOR(32)) END;");
+}
+
+TEST_F(TestParserBlackCvCParser, bad_inputs)
+{
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
+  tryBadInput("ASSERT;");  // no args
+  tryBadInput("QUERY");
+  tryBadInput("CHECKSAT");
+  tryBadInput("a, b : boolean;");  // lowercase boolean isn't a type
+  tryBadInput("0x : INT;");        // 0x isn't an identifier
+  tryBadInput(
+      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;");  // no semicolon after decl
+  tryBadInput("ASSERT 0bin012 /= 0hex0;");            // bad binary literal
+  tryBadInput("a, b: BOOLEAN; QUERY a(b);");  // non-function used as function
+  tryBadInput("a : BOOLEAN; a: INT;");        // double decl, incompatible
+  tryBadInput("A : TYPE; A: TYPE;");          // types can't be double-declared
+  tryBadInput("a : INT; a: INT = 5;");        // can't define after decl
+  tryBadInput("a : INT = 5; a: BOOLEAN;");    // decl w/ incompatible type
+  tryBadInput(
+      "a : TYPE; a : INT; a : a;");  // ok except a is both INT and sort `a'
+  tryBadInput(
+      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | "
+      "cons(car:INT,cdr:list) END;");
+  tryBadInput(
+      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil "
+      "END;");
+  tryBadInput(
+      "DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = "
+      "cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+#endif
+}
+
+TEST_F(TestParserBlackCvCParser, good_exprs)
+{
+  tryGoodExpr("a AND b");
+  tryGoodExpr("a AND b OR c");
+  tryGoodExpr("(a => b) AND a => b");
+  tryGoodExpr("(a <=> b) AND (NOT a)");
+  tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))");
+}
+
+TEST_F(TestParserBlackCvCParser, bad_exprs)
+{
+// competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
+  tryBadInput("a AND");             // wrong arity
+  tryBadInput("AND(a,b)");          // not infix
+  tryBadInput("(OR (AND a b) c)");  // not infix
+  tryBadInput("a IMPLIES b");       // should be =>
+  tryBadInput("a NOT b");           // wrong arity, not infix
+  tryBadInput("a and b");           // wrong case
+#endif
+}
+
+/* -------------------------------------------------------------------------- */
+
+class TestParserBlackSmt2Parser : public TestParserBlackParser
+{
+ protected:
+  TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {}
+};
+
+TEST_F(TestParserBlackSmt2Parser, good_inputs)
+{
+  tryGoodInput("");  // empty string is OK
+  tryGoodInput("(set-logic QF_UF)");
+  tryGoodInput("(set-info :notes |This is a note, take note!|)");
+  tryGoodInput("(set-logic QF_UF) (assert true)");
+  tryGoodInput("(check-sat)");
+  tryGoodInput("(exit)");
+  tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
+  tryGoodInput(
+      "(set-logic QF_UF) (declare-fun a () Bool) "
+      "(declare-fun b () Bool)");
+  tryGoodInput(
+      "(set-logic QF_UF) (declare-fun a () Bool) "
+      "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))");
+  tryGoodInput(
+      "(set-logic QF_UF) (declare-sort a 0) "
+      "(declare-fun f (a) a) (declare-fun x () a) "
+      "(assert (= (f x) x))");
+  tryGoodInput(
+      "(set-logic QF_UF) (declare-sort a 0) "
+      "(declare-fun x () a) (declare-fun y () a) "
+      "(assert (= (ite true x y) x))");
+  tryGoodInput(";; nothing but a comment");
+  tryGoodInput("; a comment\n(check-sat ; goodbye\n)");
+}
+
+TEST_F(TestParserBlackSmt2Parser, bad_inputs)
+{
+  // competition builds don't do any checking
+#ifndef CVC4_COMPETITION_MODE
+  // no arguments
+  tryBadInput("(assert)");
+  // illegal character in symbol
+  tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
+  // check-sat should not have an argument
+  tryBadInput("(set-logic QF_UF) (check-sat true)", true);
+  // no argument
+  tryBadInput("(declare-sort a)");
+  // double declaration
+  tryBadInput("(declare-sort a 0) (declare-sort a 0)");
+  // should be "(declare-fun p () Bool)"
+  tryBadInput("(set-logic QF_UF) (declare-fun p Bool)");
+  // strict mode
+  // no set-logic, core theory symbol "true" undefined
+  tryBadInput("(assert true)", true);
+  // core theory symbol "Bool" undefined
+  tryBadInput("(declare-fun p Bool)", true);
+#endif
+}
+
+TEST_F(TestParserBlackSmt2Parser, good_exprs)
+{
+  tryGoodExpr("(and a b)");
+  tryGoodExpr("(or (and a b) c)");
+  tryGoodExpr("(=> (and (=> a b) a) b)");
+  tryGoodExpr("(and (= a b) (not a))");
+  tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))");
+  tryGoodExpr("(ite a (f x) y)");
+  tryGoodExpr("1");
+  tryGoodExpr("0");
+  tryGoodExpr("1.5");
+  tryGoodExpr("#xfab09c7");
+  tryGoodExpr("#b0001011");
+  tryGoodExpr("(* 5 1)");
+}
+
+TEST_F(TestParserBlackSmt2Parser, bad_exprs)
+{
+// 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("(implies a b)");             // no implies in v2
+  tryBadExpr("(iff a b)");                 // no iff in v2
+  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("(if_then_else a (f x) y)");  // no if_then_else in v2
+  tryBadExpr("(a b)");                     // using non-function as function
+  tryBadExpr(".5");  // rational constants must have integer prefix
+  tryBadExpr("1.");  // rational constants must have fractional suffix
+  tryBadExpr("#x");  // hex constants must have at least one digit
+  tryBadExpr("#b");  // ditto binary constants
+  tryBadExpr("#xg0f");
+  tryBadExpr("#b9");
+  // Bad strict exprs
+  tryBadExpr("(and a)", true);   // no unary and's
+  tryBadExpr("(or a)", true);    // no unary or's
+  tryBadExpr("(* 5 01)", true);  // '01' is not a valid integer constant
+#endif
+}
+}  // namespace test
+}  // namespace CVC4
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
deleted file mode 100644
index 507ccb791..000000000
--- a/test/unit/parser/parser_black.h
+++ /dev/null
@@ -1,412 +0,0 @@
-/*********************                                                        */
-/*! \file parser_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::parser::Parser, including CVC, SMT and
- ** SMT v2 inputs.
- **
- ** Black box testing of CVC4::parser::Parser, including CVC, SMT, and
- ** SMT v2 inputs.
- **/
-
-#include <cxxtest/TestSuite.h>
-#include <sstream>
-
-#include "api/cvc4cpp.h"
-#include "base/output.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "expr/symbol_manager.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/options.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "parser/smt2/smt2.h"
-#include "smt/command.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::language::input;
-using namespace std;
-
-class ParserBlack
-{
- protected:
-  Options d_options;
-
-  /* Set up declaration context for expr inputs */
-  virtual void setupContext(Parser& parser) {
-    /* a, b, c: BOOLEAN */
-    parser.bindVar("a", d_solver->getBooleanSort());
-    parser.bindVar("b", d_solver->getBooleanSort());
-    parser.bindVar("c", d_solver->getBooleanSort());
-    /* t, u, v: TYPE */
-    api::Sort t = parser.mkSort("t");
-    api::Sort u = parser.mkSort("u");
-    api::Sort v = parser.mkSort("v");
-    /* f : t->u; g: u->v; h: v->t; */
-    parser.bindVar("f", d_solver->mkFunctionSort(t, u));
-    parser.bindVar("g", d_solver->mkFunctionSort(u, v));
-    parser.bindVar("h", d_solver->mkFunctionSort(v, t));
-    /* x:t; y:u; z:v; */
-    parser.bindVar("x", t);
-    parser.bindVar("y", u);
-    parser.bindVar("z", v);
-  }
-
-  void tryGoodInput(const string goodInput)
-  {
-    try
-    {
-      //        Debug.on("parser");
-      //         Debug.on("parser-extra");
-      //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
-      //        istringstream stream(goodInputs[i]);
-      d_symman.reset(new SymbolManager(d_solver.get()));
-      Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                           .withStringInput(goodInput)
-                           .withOptions(d_options)
-                           .withInputLanguage(d_lang)
-                           .build();
-      TS_ASSERT(!parser->done());
-      Command* cmd;
-      while ((cmd = parser->nextCommand()) != NULL)
-      {
-        Debug("parser") << "Parsed command: " << (*cmd) << endl;
-        delete cmd;
-      }
-
-      TS_ASSERT(parser->done());
-      delete parser;
-      //        Debug.off("parser");
-      //        Debug.off("parser-extra");
-    }
-    catch (Exception& e)
-    {
-      cout << "\nGood input failed:\n" << goodInput << endl << e << endl;
-      //        Debug.off("parser");
-      throw;
-    }
-  }
-
-  void tryBadInput(const string badInput, bool strictMode = false)
-  {
-    //      cerr << "Testing bad input: '" << badInput << "'\n";
-    //      Debug.on("parser");
-
-    d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(badInput)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .withStrictMode(strictMode)
-                         .build();
-    TS_ASSERT_THROWS(
-        {
-          Command* cmd;
-          while ((cmd = parser->nextCommand()) != NULL)
-          {
-            Debug("parser") << "Parsed command: " << (*cmd) << endl;
-            delete cmd;
-          }
-          cout << "\nBad input succeeded:\n" << badInput << endl;
-        },
-        const ParserException&);
-    //      Debug.off("parser");
-    delete parser;
-  }
-
-  void tryGoodExpr(const string goodExpr)
-  {
-    //    Debug.on("parser");
-    //    Debug.on("parser-extra");
-    try
-    {
-      //        cerr << "Testing good expr: '" << goodExpr << "'\n";
-      // Debug.on("parser");
-      //        istringstream stream(context + goodBooleanExprs[i]);
-
-      d_symman.reset(new SymbolManager(d_solver.get()));
-      Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                           .withStringInput(goodExpr)
-                           .withOptions(d_options)
-                           .withInputLanguage(d_lang)
-                           .build();
-
-      if (d_lang == LANG_SMTLIB_V2)
-      {
-        // Use QF_LIA to make multiplication ("*") available
-        std::unique_ptr<Command> cmd(
-            static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
-      }
-
-      TS_ASSERT(!parser->done());
-      setupContext(*parser);
-      TS_ASSERT(!parser->done());
-      api::Term e = parser->nextExpression();
-      TS_ASSERT(!e.isNull());
-      e = parser->nextExpression();
-      TS_ASSERT(parser->done());
-      TS_ASSERT(e.isNull());
-      delete parser;
-    }
-    catch (Exception& e)
-    {
-      cout << endl
-           << "Good expr failed." << endl
-           << "Input: <<" << goodExpr << ">>" << endl
-           << "Output: <<" << e << ">>" << endl;
-      throw;
-    }
-  }
-
-  /* NOTE: The check implemented here may fail if a bad expression
-   * expression string has a prefix that is parseable as a good
-   * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
-   * actually return the bit-vector 10 and ignore the tail of the
-   * input. It's more trouble than it's worth to check that the whole
-   * input was consumed here, so just be careful to avoid valid
-   * prefixes in tests.
-   */
-  void tryBadExpr(const string badExpr, bool strictMode = false)
-  {
-    //    Debug.on("parser");
-    //    Debug.on("parser-extra");
-    //      cout << "Testing bad expr: '" << badExpr << "'\n";
-
-    d_symman.reset(new SymbolManager(d_solver.get()));
-    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
-                         .withStringInput(badExpr)
-                         .withOptions(d_options)
-                         .withInputLanguage(d_lang)
-                         .withStrictMode(strictMode)
-                         .build();
-    setupContext(*parser);
-    TS_ASSERT(!parser->done());
-    TS_ASSERT_THROWS(api::Term e = parser->nextExpression();
-                     cout << endl
-                          << "Bad expr succeeded." << endl
-                          << "Input: <<" << badExpr << ">>" << endl
-                          << "Output: <<" << e << ">>" << endl;
-                     , const ParserException&);
-    delete parser;
-    //    Debug.off("parser");
-  }
-
-  ParserBlack(InputLanguage lang) :
-    d_lang(lang) {
-  }
-
-  virtual ~ParserBlack() {}
-
-  void setUp()
-  {
-    d_options.set(options::parseOnly, true);
-    // ensure the old symbol manager is deleted
-    d_symman.reset(nullptr);
-    d_solver.reset(new api::Solver(&d_options));
-  }
-
-  void tearDown()
-  {
-    d_symman.reset(nullptr);
-    d_solver.reset(nullptr);
-  }
-
- private:
-  InputLanguage d_lang;
-  std::unique_ptr<api::Solver> d_solver;
-  std::unique_ptr<SymbolManager> d_symman;
-
-}; /* class ParserBlack */
-
-class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
-  typedef ParserBlack super;
-
-public:
-  Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
-
-  void setUp() override { super::setUp(); }
-
-  void tearDown() override { super::tearDown(); }
-
-  void testGoodCvc4Inputs() {
-    tryGoodInput(""); // empty string is OK
-    tryGoodInput(";"); // no command is OK
-    tryGoodInput("ASSERT TRUE;");
-    tryGoodInput("QUERY TRUE;");
-    tryGoodInput("CHECKSAT FALSE;");
-    tryGoodInput("a, b : BOOLEAN;");
-    tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
-    tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
-    tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
-    tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];");
-    tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;");
-    tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
-    tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
-    tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
-    tryGoodInput("%% nothing but a comment");
-    tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
-    tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible
-    tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
-    tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct
-    tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a'
-    tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
-    tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;");
-    //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
-    tryGoodInput(
-        "DATATYPE trex = Foo | Bar END; DATATYPE tree = "
-        "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list "
-        "OF tree,cdr:BITVECTOR(32)) END;");
-  }
-
-  void testBadCvc4Inputs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
-    tryBadInput("ASSERT;"); // no args
-    tryBadInput("QUERY");
-    tryBadInput("CHECKSAT");
-    tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type
-    tryBadInput("0x : INT;"); // 0x isn't an identifier
-    tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl
-    tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal
-    tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function
-    tryBadInput("a : BOOLEAN; a: INT;"); // double decl, incompatible
-    tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared
-    tryBadInput("a : INT; a: INT = 5;"); // can't define after decl
-    tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type
-    tryBadInput("a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a'
-    //tryBadInput("a : [1..-1];"); // bad subrange
-    //tryBadInput("a : [0. .0];"); // bad subrange
-    //tryBadInput("a : [..0];"); // bad subrange
-    //tryBadInput("a : [0.0];"); // bad subrange
-    tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;");
-    tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;");
-    tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-
-  void testGoodCvc4Exprs() {
-    tryGoodExpr("a AND b");
-    tryGoodExpr("a AND b OR c");
-    tryGoodExpr("(a => b) AND a => b");
-    tryGoodExpr("(a <=> b) AND (NOT a)");
-    tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))");
-  }
-
-  void testBadCvc4Exprs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
-    tryBadInput("a AND"); // wrong arity
-    tryBadInput("AND(a,b)"); // not infix
-    tryBadInput("(OR (AND a b) c)"); // not infix
-    tryBadInput("a IMPLIES b"); // should be =>
-    tryBadInput("a NOT b"); // wrong arity, not infix
-    tryBadInput("a and b"); // wrong case
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-};/* class Cvc4ParserTest */
-
-class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
-  typedef ParserBlack super;
-
-public:
-  Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
-
-  void setUp() override { super::setUp(); }
-
-  void tearDown() override { super::tearDown(); }
-
-  void setupContext(Parser& parser) override
-  {
-    super::setupContext(parser);
-  }
-
-  void testGoodSmt2Inputs() {
-    tryGoodInput(""); // empty string is OK
-    tryGoodInput("(set-logic QF_UF)");
-    tryGoodInput("(set-info :notes |This is a note, take note!|)");
-    tryGoodInput("(set-logic QF_UF) (assert true)");
-    tryGoodInput("(check-sat)");
-    tryGoodInput("(exit)");
-    tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
-    tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
-                 "(declare-fun b () Bool)");
-    tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
-                 "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))");
-    tryGoodInput("(set-logic QF_UF) (declare-sort a 0) "
-                 "(declare-fun f (a) a) (declare-fun x () a) "
-                 "(assert (= (f x) x))");
-    tryGoodInput("(set-logic QF_UF) (declare-sort a 0) "
-                 "(declare-fun x () a) (declare-fun y () a) "
-                 "(assert (= (ite true x y) x))");
-    tryGoodInput(";; nothing but a comment");
-    tryGoodInput("; a comment\n(check-sat ; goodbye\n)");
-  }
-
-  void testBadSmt2Inputs() {
-// competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
-    tryBadInput("(assert)"); // no args
-    tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
-    tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg
-    tryBadInput("(declare-sort a)"); // no arg
-    tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
-    tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"
-    // strict mode
-    tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
-    tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-
-  void testGoodSmt2Exprs() {
-    tryGoodExpr("(and a b)");
-    tryGoodExpr("(or (and a b) c)");
-    tryGoodExpr("(=> (and (=> a b) a) b)");
-    tryGoodExpr("(and (= a b) (not a))");
-    tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))");
-    tryGoodExpr("(ite a (f x) y)");
-    tryGoodExpr("1");
-    tryGoodExpr("0");
-    tryGoodExpr("1.5");
-    tryGoodExpr("#xfab09c7");
-    tryGoodExpr("#b0001011");
-    tryGoodExpr("(* 5 1)");
-  }
-
-  void testBadSmt2Exprs() {
-// 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("(implies a b)"); // no implies in v2
-    tryBadExpr("(iff a b)"); // no iff in v2
-    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("(if_then_else a (f x) y)"); // no if_then_else in v2
-    tryBadExpr("(a b)"); // using non-function as function
-    tryBadExpr(".5"); // rational constants must have integer prefix
-    tryBadExpr("1."); // rational constants must have fractional suffix
-    tryBadExpr("#x"); // hex constants must have at least one digit
-    tryBadExpr("#b"); // ditto binary constants
-    tryBadExpr("#xg0f");
-    tryBadExpr("#b9");
-    // Bad strict exprs
-    tryBadExpr("(and a)", true); // no unary and's
-    tryBadExpr("(or a)", true);  // no unary or's
-    tryBadExpr("(* 5 01)", true); // '01' is not a valid integer constant
-#endif /* ! CVC4_COMPETITION_MODE */
-  }
-};/* class Smt2ParserTest */