Minor refactorings, in response to code review (Bug #73)

13 files changed, 43 insertions, 341 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6a2640080..bb665ef81 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -184,9 +184,9 @@ Type* ExprManager::mkSort(const std::string& name) {
   return d_nodeManager->mkSort(name);
 }
 
-Expr ExprManager::mkVar(Type* type, const std::string& name) {
+Expr ExprManager::mkVar(const std::string& name, Type* type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
+  return Expr(this, new Node(d_nodeManager->mkVar(name, type)));
 }
 
 Expr ExprManager::mkVar(Type* type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1c1d6dbd7..82698732c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -192,7 +192,7 @@ public:
   Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(Type* type, const std::string& name);
+  Expr mkVar(const std::string& name, Type* type);
   Expr mkVar(Type* type);
 
   /** Returns the minimum arity of the given kind. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 83f28a842..2b403ad36 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -270,11 +270,11 @@ public:
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
   /**
-   * Create a variable with the given type and name.  NOTE that no
-   * lookup is done on the name.  If you mkVar(type, "a") and then
-   * mkVar(type, "a") again, you have two variables.
+   * Create a variable with the given name and type.  NOTE that no
+   * lookup is done on the name.  If you mkVar("a", type) and then
+   * mkVar("a", type) again, you have two variables.
    */
-  Node mkVar(Type* type, const std::string& name);
+  Node mkVar(const std::string& name, Type* type);
 
   /** Create a variable with the given type. */
   Node mkVar(Type* type);
@@ -767,7 +767,7 @@ inline Node NodeManager::mkNode(Kind kind,
   return NodeBuilder<>(this, kind).append(children);
 }
 
-inline Node NodeManager::mkVar(Type* type, const std::string& name) {
+inline Node NodeManager::mkVar(const std::string& name, Type* type) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 3d9006e04..61d61821b 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -127,8 +127,6 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
   }
 
   if(recognizer->mismatchIsMissingToken(recognizer, is, follow)) {
-    // We can fake the missing token and proceed
-    //
     matchedSymbol = recognizer->getMissingSymbol(recognizer, is,
                                                  recognizer->state->exception,
                                                  ttype, follow);
@@ -136,11 +134,8 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
     recognizer->state->exception->message = (void*)ANTLR3_MISSING_TOKEN_EXCEPTION_NAME;
     recognizer->state->exception->token = matchedSymbol;
     recognizer->state->exception->expecting = ttype;
-
-    // Print out the error after we insert so that ANTLRWorks sees the
-    // token in the exception.
-    //
   }
+
   reportError(recognizer);
   Unreachable("reportError should have thrown exception in AntlrInput::recoverFromMismatchedToken");
 }
@@ -178,7 +173,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
       if(ex->expecting == ANTLR3_TOKEN_EOF) {
         ss << "Expected end of file.";
       } else {
-        ss << "Expected " << tokenNames[ex->expecting] << ".";
+        ss << "Expected " << tokenNames[ex->expecting]
+           << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
       }
     }
     break;
@@ -235,14 +231,12 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     break;
 
   case ANTLR3_NO_VIABLE_ALT_EXCEPTION:
-
     // We could not pick any alt decision from the input given
     // so god knows what happened - however when you examine your grammar,
     // you should. It means that at the point where the current token occurred
     // that the DFA indicates nowhere to go from here.
     //
-    ss << "Cannot match to any predicted input.";
-
+    ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
     break;
 
   case ANTLR3_MISMATCHED_SET_EXCEPTION:
@@ -258,7 +252,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     // possible tokens at this point, but we did not see any
     // member of that set.
     //
-    ss << "Unexpected input. Expected one of : ";
+    ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token)
+       << "'. Expected one of: ";
 
     // What tokens could we have accepted at this point in the
     // parse?
@@ -296,7 +291,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     // but found a token that ended that sequence earlier than
     // we should have done.
     //
-    ss << "Missing elements.";
+    ss << "Sequence terminated early by token: '"
+       << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
     break;
 
   default:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 428e2432e..16bde1de3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -138,7 +138,7 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
 }
   : /* A sort declaration (e.g., "T : TYPE") */
     TYPE_TOK 
-    { PARSER_STATE->newSorts(idList); 
+    { PARSER_STATE->mkSorts(idList); 
       t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
     type[t] { PARSER_STATE->mkVars(idList,t); }
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 9e8ff577e..6cc8f6d9c 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -94,7 +94,7 @@ bool ParserState::isPredicate(const std::string& name) {
 Expr 
 ParserState::mkVar(const std::string& name, Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(type, name);
+  Expr expr = d_exprManager->mkVar(name, type);
   defineVar(name,expr);
   return expr;
 }
@@ -104,7 +104,7 @@ ParserState::mkVars(const std::vector<std::string> names,
                     Type* type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type));
+    vars.push_back(mkVar(names[i],type));
   }
   return vars;
 }
@@ -126,14 +126,14 @@ ParserState::undefineVar(const std::string& name) {
 void
 ParserState::setLogic(const std::string& name) {
   if( name == "QF_UF" ) {
-    newSort("U");
+    mkSort("U");
   } else {
     Unhandled(name);
   }
 }
 
 Type*
-ParserState::newSort(const std::string& name) {
+ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
   Type* type = d_exprManager->mkSort(name);
@@ -143,10 +143,10 @@ ParserState::newSort(const std::string& name) {
 }
 
 const std::vector<Type*>
-ParserState::newSorts(const std::vector<std::string>& names) {
+ParserState::mkSorts(const std::vector<std::string>& names) {
   std::vector<Type*> types;
   for(unsigned i = 0; i < names.size(); ++i) {
-    types.push_back(newSort(names[i]));
+    types.push_back(mkSort(names[i]));
   }
   return types;
 }
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 07f85623c..dc188b7d1 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -230,13 +230,13 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  Type* newSort(const std::string& name);
+  Type* mkSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
    */
   const std::vector<Type*>
-  newSorts(const std::vector<std::string>& names);
+  mkSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index c0b184abf..160bd321f 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -322,7 +322,7 @@ sortDeclaration
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      PARSER_STATE->newSort(name); }
+      PARSER_STATE->mkSort(name); }
   ;
   
 /**
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
index 03d4ba31c..936381cd6 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
@@ -51,8 +51,8 @@ public:
     try {
       d_em = new ExprManager;
 
-      a = new Expr(d_em->mkVar(d_em->booleanType(), "a"));
-      b = new Expr(d_em->mkVar(d_em->booleanType(), "b"));
+      a = new Expr(d_em->mkVar("a",d_em->booleanType()));
+      b = new Expr(d_em->mkVar("b", d_em->booleanType()));
       c = new Expr(d_em->mkExpr(MULT, *a, *b));
       mult = new Expr(d_em->mkConst(MULT));
       plus = new Expr(d_em->mkConst(PLUS));
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 9e199aa9a..17657683d 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -215,8 +215,8 @@ public:
     /* We don't have access to the ids so we can't test the implementation
      * in the black box tests. */
 
-    Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a");
-    Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b");
+    Node a = d_nodeManager->mkVar("a", d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkVar("b", d_nodeManager->booleanType());
 
     TS_ASSERT(a<b || b<a);
     TS_ASSERT(!(a<b && b<a));
@@ -492,10 +492,10 @@ public:
   void testToString() {
     Type* booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar(booleanType, "w");
-    Node x = d_nodeManager->mkVar(booleanType, "x");
-    Node y = d_nodeManager->mkVar(booleanType, "y");
-    Node z = d_nodeManager->mkVar(booleanType, "z");
+    Node w = d_nodeManager->mkVar("w",booleanType);
+    Node x = d_nodeManager->mkVar("x",booleanType);
+    Node y = d_nodeManager->mkVar("y",booleanType);
+    Node z = d_nodeManager->mkVar("z",booleanType);
     Node m = NodeBuilder<>() << w << x << kind::OR;
     Node n = NodeBuilder<>() << m << y << z << kind::AND;
 
@@ -505,10 +505,10 @@ public:
   void testToStream() {
     Type* booleanType = d_nodeManager->booleanType();
 
-    Node w = d_nodeManager->mkVar(booleanType, "w");
-    Node x = d_nodeManager->mkVar(booleanType, "x");
-    Node y = d_nodeManager->mkVar(booleanType, "y");
-    Node z = d_nodeManager->mkVar(booleanType, "z");
+    Node w = d_nodeManager->mkVar("w",booleanType);
+    Node x = d_nodeManager->mkVar("x",booleanType);
+    Node y = d_nodeManager->mkVar("y",booleanType);
+    Node z = d_nodeManager->mkVar("z",booleanType);
     Node m = NodeBuilder<>() << x << y << kind::OR;
     Node n = NodeBuilder<>() << w << m << z << kind::AND;
     Node o = NodeBuilder<>() << n << n << kind::XOR;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
deleted file mode 100644
index 5a341830b..000000000
--- a/test/unit/parser/parser_black.h
+++ /dev/null
@@ -1,294 +0,0 @@
-/*********************                                                        */
-/** parser_black.h
- ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): dejan, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Black box testing of CVC4::parser::SmtParser.
- **/
-
-#include <cxxtest/TestSuite.h>
-//#include <string>
-#include <sstream>
-
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "parser/input.h"
-#include "expr/command.h"
-#include "util/output.h"
-
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace std;
-
-
-/************************** CVC test inputs ********************************/
-
-const string goodCvc4Inputs[] = {
-      "", // empty string is OK
-      "ASSERT TRUE;",
-      "QUERY TRUE;",
-      "CHECKSAT FALSE;",
-      "a, b : BOOLEAN;",
-      "a, b : BOOLEAN; QUERY (a => b) AND a => b;",
-      "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;",
-      "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;",
-      "%% nothing but a comment",
-      "% a comment\nASSERT TRUE; %a command\n% another comment",
-  };
-
-const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string);
-
-
-/* The following expressions are valid after setupContext. */
-const string goodCvc4Exprs[] = {
-    "a AND b",
-    "a AND b OR c",
-    "(a => b) AND a => b",
-    "(a <=> b) AND (NOT a)",
-    "(a XOR b) <=> (a OR b) AND (NOT (a AND b))"
-};
-
-const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string);
-
-const string badCvc4Inputs[] = {
-      ";", // no command
-      "ASSERT;", // no args
-      "QUERY",
-      "CHECKSAT",
-      "a, b : boolean;", // lowercase boolean isn't a type
-      "0x : INT;", // 0x isn't an identifier
-      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl
-      "a : BOOLEAN; a: BOOLEAN;" // double decl
-      "a, b: BOOLEAN; QUERY a(b);" // non-function used as function
-  };
-
-const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string);
-
-/* The following expressions are invalid even after setupContext. */
-const string badCvc4Exprs[] = {
-    "a AND", // wrong arity
-    "AND(a,b)", // not infix
-    "(OR (AND a b) c)", // not infix
-    "a IMPLIES b", // should be =>
-    "a NOT b", // wrong arity, not infix
-    "a and b" // wrong case
-};
-
-const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string);
-
-/************************** SMT test inputs ********************************/
-
-const string goodSmtInputs[] = {
-    "", // empty string is OK
-    "(benchmark foo :assumption true)",
-    "(benchmark bar :formula true)",
-    "(benchmark qux :formula false)",
-    "(benchmark baz :extrapreds ( (a) (b) ) )",
-    "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))",
-    "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) )  :formula (= (f x) x))",
-    "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))",
-    ";; nothing but a comment",
-    "; a comment\n(benchmark foo ; hello\n  :formula true; goodbye\n)"
-  };
-
-const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string);
-
-/* The following expressions are valid after setupContext. */
-const string goodSmtExprs[] = {
-    "(and a b)",
-    "(or (and a b) c)",
-    "(implies (and (implies a b) a) b)",
-    "(and (iff a b) (not a))",
-    "(iff (xor a b) (and (or a b) (not (and a b))))",
-    "(ite a (f x) y)",
-    "(if_then_else a (f x) y)"
-};
-
-const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string);
-
-const string badSmtInputs[] = {
-    "(benchmark foo)", // empty benchmark is not OK
-    "(benchmark bar :assumption)", // no args
-    "(benchmark bar :formula)",
-    "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl
-    "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens
-  };
-
-const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string);
-
-/* The following expressions are invalid even after setupContext. */
-const string badSmtExprs[] = {
-    "(and)", // wrong arity
-    "(and a b", // no closing paren
-    "(a and b)", // infix
-    "(OR (AND a b) c)", // wrong case
-    "(a IMPLIES b)", // infix AND wrong case
-    "(not a b)", // wrong arity
-    "not a", // needs parens
-    "(ite a x)", // wrong arity
-    "(a b)" // using non-function as function
-};
-
-const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
-
-class ParserBlack : public CxxTest::TestSuite {
-  ExprManager *d_exprManager;
-
-  /* Set up declaration context for expr inputs */
-
-  void setupContext(Input* input) {
-    /* a, b, c: BOOLEAN */
-    input->mkVar("a",(Type*)d_exprManager->booleanType());
-    input->mkVar("b",(Type*)d_exprManager->booleanType());
-    input->mkVar("c",(Type*)d_exprManager->booleanType());
-    /* t, u, v: TYPE */
-    Type *t = input->newSort("t");
-    Type *u = input->newSort("u");
-    Type *v = input->newSort("v");
-    /* f : t->u; g: u->v; h: v->t; */
-    input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
-    input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
-    input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
-    /* x:t; y:u; z:v; */
-    input->mkVar("x",t);
-    input->mkVar("y",u);
-    input->mkVar("z",v);
-  }
-
-  void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
-    for(int i = 0; i < numInputs; ++i) {
-      try {
-//         Debug.on("parser");
-//         Debug.on("parser-extra");
-         Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n";
-//        istringstream stream(goodInputs[i]);
-        Input* parser = Input::newStringParser(d_exprManager, d_lang, goodInputs[i], "test");
-        TS_ASSERT( !parser->done() );
-        Command* cmd;
-        while((cmd = parser->parseNextCommand())) {
-          // cout << "Parsed command: " << (*cmd) << endl;
-        }
-        TS_ASSERT( parser->parseNextCommand() == NULL );
-        TS_ASSERT( parser->done() );
-        delete parser;
-//        Debug.off("parser");
-//        Debug.off("parser-extra");
-      } catch (Exception& e) {
-        cout << "\nGood input failed:\n" << goodInputs[i] << endl
-             << e << endl;
-//        Debug.off("parser-extra");
-        throw;
-      }
-    }
-  }
-
-  void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) {
-    for(int i = 0; i < numInputs; ++i) {
-//      cout << "Testing bad input: '" << badInputs[i] << "'\n";
-//      Debug.on("parser");
-      Input* parser = Input::newStringParser(d_exprManager, d_lang, badInputs[i], "test");
-      TS_ASSERT_THROWS
-        ( while(parser->parseNextCommand());
-          cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, 
-          ParserException );
-//      Debug.off("parser");
-      delete parser;
-    }
-  }
-
-  void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) {
-    // cout << "Using context: " << context << endl;
-//    Debug.on("parser");
-//    Debug.on("parser-extra");
-    for(int i = 0; i < numExprs; ++i) {
-      try {
-        // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n";
-        // Debug.on("parser");
-//        istringstream stream(context + goodBooleanExprs[i]);
-        Input* parser = Input::newStringParser(d_exprManager, d_lang,
-                                              goodBooleanExprs[i], "test");
-        TS_ASSERT( !parser->done() );
-        setupContext(parser);
-        TS_ASSERT( !parser->done() );
-        Expr e = parser->parseNextExpression();
-        TS_ASSERT( !e.isNull() );
-        e = parser->parseNextExpression();
-        TS_ASSERT( parser->done() );
-        TS_ASSERT( e.isNull() );
-        delete parser;
-      } catch (Exception& e) {
-        cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl;
-        cout << e;
-        throw e;
-      }
-    }
-  }
-
-  void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) {
-    //Debug.on("parser");
-    for(int i = 0; i < numExprs; ++i) {
-      // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n";
-//      istringstream stream(context + badBooleanExprs[i]);
-      Input* parser = Input::newStringParser(d_exprManager, d_lang,
-                                             badBooleanExprs[i], "test");
-
-      TS_ASSERT( !parser->done() );
-      setupContext(parser);
-      TS_ASSERT( !parser->done() );
-      TS_ASSERT_THROWS
-        ( parser->parseNextExpression();
-          cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, 
-          ParserException );
-      delete parser;
-    }
-    //Debug.off("parser");
-  }
-
-public:
-  void setUp() {
-    d_exprManager = new ExprManager();
-  }
-
-  void tearDown() {
-    delete d_exprManager;
-  }
-
-  void testGoodCvc4Inputs() {
-    tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
-  }
-
-  void testBadCvc4Inputs() {
-    tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs);
-  }
-
-  void testGoodCvc4Exprs() {
-    tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs);
-  }
-
-  void testBadCvc4Exprs() {
-    tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs);
-  }
-
-  void testGoodSmtInputs() {
-    tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs);
-  }
-
-  void testBadSmtInputs() {
-    tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs);
-  }
-
-  void testGoodSmtExprs() {
-    tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs);
-  }
-
-  void testBadSmtExprs() {
-    tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs);
-  }
-};
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h
index 270061c29..d0959cf6f 100644
--- a/test/unit/parser/parser_white.h
+++ b/test/unit/parser/parser_white.h
@@ -150,9 +150,9 @@ class ParserWhite : public CxxTest::TestSuite {
     parserState->mkVar("b",(Type*)d_exprManager->booleanType());
     parserState->mkVar("c",(Type*)d_exprManager->booleanType());
     /* t, u, v: TYPE */
-    Type *t = parserState->newSort("t");
-    Type *u = parserState->newSort("u");
-    Type *v = parserState->newSort("v");
+    Type *t = parserState->mkSort("t");
+    Type *u = parserState->mkSort("u");
+    Type *v = parserState->mkSort("v");
     /* f : t->u; g: u->v; h: v->t; */
     parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
     parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index c6da48291..905294c27 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -214,8 +214,8 @@ public:
     Type* typeX = d_nm->booleanType();
     Type* typeF = d_nm->mkFunctionType(typeX, typeX);
 
-    Node x = d_nm->mkVar(typeX, "x");
-    Node f = d_nm->mkVar(typeF, "f");
+    Node x = d_nm->mkVar("x",typeX);
+    Node f = d_nm->mkVar("f",typeF);
     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
     Node f_x_eq_x = f_x.eqNode(x);