Plug solver API object into parser. (#2240)

5 files changed, 241 insertions, 238 deletions

diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 1df405a17..a135e6c6c 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -2,7 +2,7 @@
 /*! \file ouroborous.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters, Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -28,6 +28,7 @@
 #include <sstream>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "options/set_language.h"
@@ -108,12 +109,12 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL
 
 
 int runTest() {
-  ExprManager em;
-  psr =
-    ParserBuilder(&em, "internal-buffer")
-      .withStringInput(declarations)
-      .withInputLanguage(input::LANG_SMTLIB_V2)
-      .build();
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver());
+  psr = ParserBuilder(solver.get(), "internal-buffer")
+            .withStringInput(declarations)
+            .withInputLanguage(input::LANG_SMTLIB_V2)
+            .build();
 
   // we don't need to execute them, but we DO need to parse them to
   // get the declarations
diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
index 134185dc4..8a14094d3 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/system/smt2_compliance.cpp
@@ -2,7 +2,7 @@
 /*! \file smt2_compliance.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters, Aina Niemetz, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -18,6 +18,7 @@
 #include <iostream>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
 #include "options/set_language.h"
@@ -30,43 +31,45 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace std;
 
-void testGetInfo(SmtEngine& smt, const char* s);
+void testGetInfo(api::Solver* solver, const char* s);
 
-int main() {
+int main()
+{
   Options opts;
   opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
   opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
 
-  ExprManager em(opts);
-  SmtEngine smt(&em);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&opts));
 
-  testGetInfo(smt, ":error-behavior");
-  testGetInfo(smt, ":name");
-  testGetInfo(smt, ":authors");
-  testGetInfo(smt, ":version");
-  testGetInfo(smt, ":status");
-  testGetInfo(smt, ":reason-unknown");
-  testGetInfo(smt, ":arbitrary-undefined-keyword");
-  testGetInfo(smt, ":56");// legal
-  testGetInfo(smt, ":<=");// legal
-  testGetInfo(smt, ":->");// legal
-  testGetInfo(smt, ":all-statistics");
+  testGetInfo(solver.get(), ":error-behavior");
+  testGetInfo(solver.get(), ":name");
+  testGetInfo(solver.get(), ":authors");
+  testGetInfo(solver.get(), ":version");
+  testGetInfo(solver.get(), ":status");
+  testGetInfo(solver.get(), ":reason-unknown");
+  testGetInfo(solver.get(), ":arbitrary-undefined-keyword");
+  testGetInfo(solver.get(), ":56");  // legal
+  testGetInfo(solver.get(), ":<=");  // legal
+  testGetInfo(solver.get(), ":->");  // legal
+  testGetInfo(solver.get(), ":all-statistics");
 
   return 0;
 }
 
-void testGetInfo(SmtEngine& smt, const char* s) {
-  ParserBuilder pb(smt.getExprManager(), "<internal>",
-                   smt.getExprManager()->getOptions());
+void testGetInfo(api::Solver* solver, const char* s)
+{
+  ParserBuilder pb(
+      solver, "<internal>", solver->getExprManager()->getOptions());
   Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
   assert(p != NULL);
   Command* c = p->nextCommand();
   assert(c != NULL);
   cout << c << endl;
   stringstream ss;
-  c->invoke(&smt, ss);
+  c->invoke(solver->getSmtEngine(), ss);
   assert(p->nextCommand() == NULL);
   delete p;
   delete c;
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index cf68b5465..44b3660c9 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Christopher L. Conway, Aina Niemetz, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -20,6 +20,7 @@
 #include <vector>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "main/interactive_shell.h"
 #include "options/base_options.h"
@@ -31,64 +32,38 @@
 using namespace CVC4;
 using namespace std;
 
-class InteractiveShellBlack : public CxxTest::TestSuite {
-private:
-  ExprManager* d_exprManager;
-  Options d_options;
-  stringstream* d_sin;
-  stringstream* d_sout;
-
-  /**
-   * Read up to maxCommands+1 from the shell and throw an assertion error if
-   * it's fewer than minCommands and more than maxCommands.
-   * Note that an empty string followed by EOF may be returned as an empty
-   * command, and not NULL (subsequent calls to readCommand() should return
-   * NULL). E.g., "CHECKSAT;\n" may return two commands: the CHECKSAT,
-   * followed by an empty command, followed by NULL.
-   */
-  void countCommands(InteractiveShell& shell, 
-                     int minCommands, 
-                     int maxCommands) {
-    Command* cmd;
-    int n = 0;
-    while( n <= maxCommands && (cmd = shell.readCommand()) != NULL ) {
-      ++n;
-      delete cmd;
-    }
-    TS_ASSERT( n <= maxCommands );
-    TS_ASSERT( n >= minCommands );
-  }
-
+class InteractiveShellBlack : public CxxTest::TestSuite
+{
  public:
-  void setUp() {
+  void setUp()
+  {
     d_sin = new stringstream;
     d_sout = new stringstream;
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
-    d_exprManager = new ExprManager(d_options);
+    d_solver.reset(new api::Solver(&d_options));
   }
 
   void tearDown() {
-    delete d_exprManager;
     delete d_sin;
     delete d_sout;
   }
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
     /* readCommand may return a sequence, so we can't say for sure
        whether it will return 1 or 2... */
@@ -96,7 +71,7 @@ private:
   }
 
   void testDefUse2() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -106,16 +81,42 @@ private:
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(*d_exprManager);
+    InteractiveShell shell(d_solver.get());
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }
 
+ private:
+  std::unique_ptr<api::Solver> d_solver;
+  Options d_options;
+  stringstream* d_sin;
+  stringstream* d_sout;
+
+  /**
+   * Read up to maxCommands+1 from the shell and throw an assertion error if
+   * it's fewer than minCommands and more than maxCommands.  Note that an empty
+   * string followed by EOF may be returned as an empty command, and not NULL
+   * (subsequent calls to readCommand() should return NULL). E.g., "CHECKSAT;\n"
+   * may return two commands: the CHECKSAT, followed by an empty command,
+   * followed by NULL.
+   */
+  void countCommands(InteractiveShell& shell, int minCommands, int maxCommands)
+  {
+    Command* cmd;
+    int n = 0;
+    while (n <= maxCommands && (cmd = shell.readCommand()) != NULL)
+    {
+      ++n;
+      delete cmd;
+    }
+    TS_ASSERT(n <= maxCommands);
+    TS_ASSERT(n >= minCommands);
+  }
 };
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index b3c36e2c4..7b52e0662 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -2,7 +2,7 @@
 /*! \file parser_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Tim King
+ **   Christopher L. Conway, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -19,6 +19,7 @@
 #include <cxxtest/TestSuite.h>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
@@ -36,69 +37,71 @@ using namespace CVC4::parser;
 using namespace CVC4::language::input;
 using namespace std;
 
-class ParserBlack {
-  InputLanguage d_lang;
-  ExprManager *d_exprManager;
-
-protected:
+class ParserBlack
+{
+ protected:
   Options d_options;
 
   /* Set up declaration context for expr inputs */
   virtual void setupContext(Parser& parser) {
     /* a, b, c: BOOLEAN */
-    parser.mkVar("a",d_exprManager->booleanType());
-    parser.mkVar("b",d_exprManager->booleanType());
-    parser.mkVar("c",d_exprManager->booleanType());
+    parser.mkVar("a", d_solver->getExprManager()->booleanType());
+    parser.mkVar("b", d_solver->getExprManager()->booleanType());
+    parser.mkVar("c", d_solver->getExprManager()->booleanType());
     /* t, u, v: TYPE */
     Type t = parser.mkSort("t");
     Type u = parser.mkSort("u");
     Type v = parser.mkSort("v");
     /* f : t->u; g: u->v; h: v->t; */
-    parser.mkVar("f", d_exprManager->mkFunctionType(t,u));
-    parser.mkVar("g", d_exprManager->mkFunctionType(u,v));
-    parser.mkVar("h", d_exprManager->mkFunctionType(v,t));
+    parser.mkVar("f", d_solver->getExprManager()->mkFunctionType(t, u));
+    parser.mkVar("g", d_solver->getExprManager()->mkFunctionType(u, v));
+    parser.mkVar("h", d_solver->getExprManager()->mkFunctionType(v, t));
     /* x:t; y:u; z:v; */
     parser.mkVar("x",t);
     parser.mkVar("y",u);
     parser.mkVar("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]);
-        Parser *parser =
-          ParserBuilder(d_exprManager,"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 tryGoodInput(const string goodInput)
+  {
+    try
+    {
+      //        Debug.on("parser");
+      //         Debug.on("parser-extra");
+      //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
+      //        istringstream stream(goodInputs[i]);
+      Parser* parser = ParserBuilder(d_solver.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");
+  void tryBadInput(const string badInput, bool strictMode = false)
+  {
+    //      cerr << "Testing bad input: '" << badInput << "'\n";
+    //      Debug.on("parser");
 
-    Parser* parser = ParserBuilder(d_exprManager, "test")
+    Parser* parser = ParserBuilder(d_solver.get(), "test")
                          .withStringInput(badInput)
                          .withOptions(d_options)
                          .withInputLanguage(d_lang)
@@ -107,7 +110,8 @@ protected:
     TS_ASSERT_THROWS(
         {
           Command* cmd;
-          while ((cmd = parser->nextCommand()) != NULL) {
+          while ((cmd = parser->nextCommand()) != NULL)
+          {
             Debug("parser") << "Parsed command: " << (*cmd) << endl;
             delete cmd;
           }
@@ -118,37 +122,40 @@ protected:
     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]);
-
-        Parser *parser =
-          ParserBuilder(d_exprManager,"test")
-            .withStringInput(goodExpr)
-            .withOptions(d_options)
-            .withInputLanguage(d_lang)
-            .build();
-
-        TS_ASSERT( !parser->done() );
-        setupContext(*parser);
-        TS_ASSERT( !parser->done() );
-        Expr 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;
-      }
+  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]);
+
+      Parser* parser = ParserBuilder(d_solver.get(), "test")
+                           .withStringInput(goodExpr)
+                           .withOptions(d_options)
+                           .withInputLanguage(d_lang)
+                           .build();
+
+      TS_ASSERT(!parser->done());
+      setupContext(*parser);
+      TS_ASSERT(!parser->done());
+      Expr 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
@@ -159,44 +166,48 @@ protected:
    * 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";
-
-      Parser *parser =
-        ParserBuilder(d_exprManager,"test")
-          .withStringInput(badExpr)
-          .withOptions(d_options)
-          .withInputLanguage(d_lang)
-          .withStrictMode(strictMode)
-          .build();
-      setupContext(*parser);
-      TS_ASSERT( !parser->done() );
-      TS_ASSERT_THROWS
-        ( Expr e = parser->nextExpression();
-          cout << endl
-               << "Bad expr succeeded." << endl
-               << "Input: <<" << badExpr << ">>" << endl
-               << "Output: <<" << e << ">>" << endl;,
-          const ParserException& );
-      delete parser;
-//    Debug.off("parser");
+  void tryBadExpr(const string badExpr, bool strictMode = false)
+  {
+    //    Debug.on("parser");
+    //    Debug.on("parser-extra");
+    //      cout << "Testing bad expr: '" << badExpr << "'\n";
+
+    Parser* parser = ParserBuilder(d_solver.get(), "test")
+                         .withStringInput(badExpr)
+                         .withOptions(d_options)
+                         .withInputLanguage(d_lang)
+                         .withStrictMode(strictMode)
+                         .build();
+    setupContext(*parser);
+    TS_ASSERT(!parser->done());
+    TS_ASSERT_THROWS(Expr 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) {
   }
 
-  void setUp() {
-    d_exprManager = new ExprManager;
+  void setUp()
+  {
     d_options.set(options::parseOnly, true);
+    d_solver.reset(new api::Solver(&d_options));
   }
 
   void tearDown() {
-    delete d_exprManager;
   }
-};/* class ParserBlack */
+
+ private:
+  InputLanguage d_lang;
+  std::unique_ptr<api::Solver> d_solver;
+
+}; /* class ParserBlack */
 
 class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
   typedef ParserBlack super;
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 066c45fe1..45baf177f 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -2,7 +2,7 @@
 /*! \file parser_builder_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Tim King, Morgan Deters
+ **   Christopher L. Conway, Aina Niemetz, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -24,6 +24,7 @@
 #include <fstream>
 #include <iostream>
 
+#include "api/cvc4cpp.h"
 #include "options/language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -34,57 +35,19 @@ using namespace CVC4::parser;
 using namespace CVC4::language::input;
 using namespace std;
 
-class ParserBuilderBlack : public CxxTest::TestSuite {
+class ParserBuilderBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() { d_solver.reset(new api::Solver()); }
 
-  ExprManager *d_exprManager;
+  void tearDown() {}
 
-  void checkEmptyInput(ParserBuilder& builder) {
-    Parser *parser = builder.build();
-    TS_ASSERT( parser != NULL );
-
-    Expr e = parser->nextExpression();
-    TS_ASSERT( e.isNull() );
-
-    delete parser;
-  }
-
-  void checkTrueInput(ParserBuilder& builder) {
-    Parser *parser = builder.build();
-    TS_ASSERT( parser != NULL );
-
-    Expr e = parser->nextExpression();
-    TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) );
-
-    e = parser->nextExpression();
-    TS_ASSERT( e.isNull() );
-    delete parser;
-  }
-
-  char* mkTemp() {
-    char *filename = strdup("/tmp/testinput.XXXXXX");
-    int fd = mkstemp(filename);
-    TS_ASSERT( fd != -1 );
-    close(fd);
-    return filename;
-  }
-
-public:
-
-  void setUp() {
-    d_exprManager = new ExprManager;
-  }
-
-  void tearDown() {
-    delete d_exprManager;
-  }
-
-  void testEmptyFileInput() {
+  void testEmptyFileInput()
+  {
     char *filename = mkTemp();
 
     checkEmptyInput(
-      ParserBuilder(d_exprManager,filename)
-        .withInputLanguage(LANG_CVC4)
-                    );
+        ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
 
     remove(filename);
     free(filename);
@@ -98,48 +61,72 @@ public:
     fs.close();
 
     checkTrueInput(
-      ParserBuilder(d_exprManager,filename)
-        .withInputLanguage(LANG_CVC4)
-                   );
+        ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
 
     remove(filename);
     free(filename);
   }
 
   void testEmptyStringInput() {
-    checkEmptyInput(
-      ParserBuilder(d_exprManager,"foo")
-        .withInputLanguage(LANG_CVC4)
-        .withStringInput("")
-                    );
+    checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+                        .withInputLanguage(LANG_CVC4)
+                        .withStringInput(""));
   }
 
   void testTrueStringInput() {
-    checkTrueInput(
-      ParserBuilder(d_exprManager,"foo")
-        .withInputLanguage(LANG_CVC4)
-        .withStringInput("TRUE")
-                   );
+    checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+                       .withInputLanguage(LANG_CVC4)
+                       .withStringInput("TRUE"));
   }
 
   void testEmptyStreamInput() {
     stringstream ss( "", ios_base::in );
-    checkEmptyInput(
-      ParserBuilder(d_exprManager,"foo")
-        .withInputLanguage(LANG_CVC4)
-        .withStreamInput(ss)
-                    );
+    checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+                        .withInputLanguage(LANG_CVC4)
+                        .withStreamInput(ss));
   }
 
   void testTrueStreamInput() {
     stringstream ss( "TRUE", ios_base::in );
-    checkTrueInput(
-      ParserBuilder(d_exprManager,"foo")
-        .withInputLanguage(LANG_CVC4)
-        .withStreamInput(ss)
-                   );
+    checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+                       .withInputLanguage(LANG_CVC4)
+                       .withStreamInput(ss));
   }
 
+ private:
+  void checkEmptyInput(ParserBuilder &builder)
+  {
+    Parser *parser = builder.build();
+    TS_ASSERT(parser != NULL);
+
+    Expr e = parser->nextExpression();
+    TS_ASSERT(e.isNull());
+
+    delete parser;
+  }
+
+  void checkTrueInput(ParserBuilder &builder)
+  {
+    Parser *parser = builder.build();
+    TS_ASSERT(parser != NULL);
+
+    Expr e = parser->nextExpression();
+    TS_ASSERT_EQUALS(e, d_solver->getExprManager()->mkConst(true));
+
+    e = parser->nextExpression();
+    TS_ASSERT(e.isNull());
+    delete parser;
+  }
+
+  char *mkTemp()
+  {
+    char *filename = strdup("/tmp/testinput.XXXXXX");
+    int fd = mkstemp(filename);
+    TS_ASSERT(fd != -1);
+    close(fd);
+    return filename;
+  }
 
+  std::unique_ptr<api::Solver> d_solver;
 
 }; // class ParserBuilderBlack