Plug solver API object into parser. (#2240)

35 files changed, 842 insertions, 626 deletions

diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index d12f2877e..6ce35b300 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -2,7 +2,7 @@ noinst_DATA =
 
 if CVC4_LANGUAGE_BINDING_JAVA
 noinst_DATA += \
-	CVC4Streams.class \
+	#CVC4Streams.class \  ## disabled until bindings for the new API are in place (issue #2284)
 	BitVectors.class \
 	BitVectorsAndArrays.class \
 	Combination.class \
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index a9c18c3ae..a6c146622 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -2,7 +2,7 @@
 /*! \file normalize.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Dejan Jovanovic, 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.
@@ -22,6 +22,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
@@ -29,8 +30,8 @@
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "smt/smt_engine.h"
 #include "smt/command.h"
+#include "smt/smt_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -46,18 +47,16 @@ int main(int argc, char* argv[])
   // Create the expression manager
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2)
        << expr::ExprSetDepth(-1);
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
-  // Smt manager for simplifications
-  SmtEngine engine(&exprManager);
-
   // Variables and assertions
   vector<Expr> assertions;
 
@@ -66,7 +65,7 @@ int main(int argc, char* argv[])
 
     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
     if (assert) {
-      Expr normalized = engine.simplify(assert->getExpr());
+      Expr normalized = solver->getSmtEngine()->simplify(assert->getExpr());
       cout << "(assert " << normalized << ")" << endl;
       delete cmd;
       continue;
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index 1ece6a86d..55ddb0997 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -2,7 +2,7 @@
 /*! \file smt2info.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Dejan Jovanovic, 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.
@@ -21,6 +21,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/options.h"
 #include "parser/parser.h"
@@ -78,10 +79,11 @@ int main(int argc, char* argv[])
     // Create the expression manager
     Options options;
     options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-    ExprManager exprManager(options);
+    std::unique_ptr<api::Solver> solver =
+        std::unique_ptr<api::Solver>(new api::Solver(&options));
 
     // Create the parser
-    ParserBuilder parserBuilder(&exprManager, input, options);
+    ParserBuilder parserBuilder(solver.get(), input, options);
     Parser* parser = parserBuilder.build();
 
     // Variables and assertions
@@ -122,7 +124,9 @@ int main(int argc, char* argv[])
   
     unsigned total_degree = 0;
     for (unsigned i = 0; i < assertions.size(); ++ i) {
-      total_degree = std::max(total_degree, compute_degree(exprManager, assertions[i]));
+      total_degree =
+          std::max(total_degree,
+                   compute_degree(*solver->getExprManager(), assertions[i]));
     }
   
     cout << "degree: " << total_degree << endl;
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 94cb23a79..04a33624c 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -2,7 +2,7 @@
 /*! \file smt2todreal.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Dejan Jovanovic, 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.
@@ -22,13 +22,14 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "smt/smt_engine.h"
 #include "smt/command.h"
+#include "smt/smt_engine.h"
 
 using namespace std;
 using namespace CVC4;
@@ -45,17 +46,15 @@ int main(int argc, char* argv[])
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
   options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   cout << expr::ExprDag(0) << expr::ExprSetDepth(-1);
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
-  // Smt manager for simplifications
-  SmtEngine engine(&exprManager);
-
   // Variables and assertions
   std::map<Expr, unsigned> variables;
   vector<string> info_tags;
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 767da1ffd..c4649dcae 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -2,7 +2,7 @@
 /*! \file smt2toisat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Andrew Reynolds
+ **   Dejan Jovanovic, 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.
@@ -22,6 +22,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/options.h"
 #include "parser/parser.h"
@@ -50,15 +51,13 @@ int main(int argc, char* argv[])
   // Create the expression manager
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
-  // Smt manager for simplifications
-  SmtEngine engine(&exprManager);
-
   // Variables and assertions
   std::map<Expr, unsigned> variables;
   vector<string> info_tags;
@@ -88,7 +87,7 @@ int main(int argc, char* argv[])
     
     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
     if (assert) {
-      assertions.push_back(engine.simplify(assert->getExpr()));
+      assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr()));
       delete cmd;
       continue;
     }
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index b60c4824b..fd344caa9 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -22,6 +22,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/options.h"
 #include "parser/parser.h"
@@ -48,10 +49,11 @@ int main(int argc, char* argv[])
   // Create the expression manager
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
   // Variables and assertions
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index aea436383..acfd6bf97 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -22,6 +22,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/options.h"
 #include "parser/parser.h"
@@ -49,10 +50,11 @@ int main(int argc, char* argv[])
   // Create the expression manager
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
   // Variables and assertions
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index b7bbc5a75..feb5a583a 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -2,7 +2,7 @@
 /*! \file smt2toredlog.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Andrew Reynolds
+ **   Dejan Jovanovic, 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.
@@ -22,6 +22,7 @@
 #include <typeinfo>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/options.h"
 #include "parser/parser.h"
@@ -53,15 +54,13 @@ int main(int argc, char* argv[])
   // Create the expression manager
   Options options;
   options.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  ExprManager exprManager(options);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&options));
 
   // Create the parser
-  ParserBuilder parserBuilder(&exprManager, input, options);
+  ParserBuilder parserBuilder(solver.get(), input, options);
   Parser* parser = parserBuilder.build();
 
-  // Smt manager for simplifications
-  SmtEngine engine(&exprManager);
-
   // Variables and assertions
   std::map<Expr, unsigned> variables;
   vector<string> info_tags;
@@ -91,7 +90,7 @@ int main(int argc, char* argv[])
     
     AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
     if (assert) {
-      assertions.push_back(engine.simplify(assert->getExpr()));
+      assertions.push_back(solver->getSmtEngine()->simplify(assert->getExpr()));
       delete cmd;
       continue;
     }
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index f5398f4df..452a874a8 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -2,7 +2,7 @@
 /*! \file sets_translate.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Tim King, Mathias Preiner
+ **   Kshitij Bansal, 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.
@@ -23,6 +23,7 @@
 #include <unordered_map>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "options/language.h"
 #include "options/options.h"
@@ -268,12 +269,13 @@ int main(int argc, char* argv[])
     options.setInputLanguage(language::input::LANG_SMTLIB_V2);
     cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
     // cout << Expr::dag(0);
-    ExprManager exprManager(options);
+    std::unique_ptr<api::Solver> solver =
+        std::unique_ptr<api::Solver>(new api::Solver(&options));
 
-    Mapper m(&exprManager);
+    Mapper m(solver->getExprManager());
 
     // Create the parser
-    ParserBuilder parserBuilder(&exprManager, input, options);
+    ParserBuilder parserBuilder(solver.get(), input, options);
     if(input == "<stdin>") parserBuilder.withStreamInput(cin);
     Parser* parser = parserBuilder.build();
 
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 1de05f65a..5be837e63 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -2,7 +2,7 @@
 /*! \file translator.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.
@@ -22,6 +22,7 @@
 #include <getopt.h>
 #include <iostream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "options/language.h"
@@ -105,7 +106,9 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag
   Options opts;
   opts.setInputLanguage(fromLang);
   ExprManager exprMgr(opts);
-  ParserBuilder parserBuilder(&exprMgr, filename, opts);
+  std::unique_ptr<api::Solver> solver =
+      std::unique_ptr<api::Solver>(new api::Solver(&opts));
+  ParserBuilder parserBuilder(solver.get(), filename, opts);
   if(!strcmp(filename, "-")) {
     parserBuilder.withFilename("<stdin>");
     parserBuilder.withLineBufferedStreamInput(cin);
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 19d7840a8..bc696a057 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -95,6 +95,10 @@ std::string Result::getUnknownExplanation(void) const
 
 std::string Result::toString(void) const { return d_result->toString(); }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Result Result::getResult(void) const { return *d_result; }
+
 std::ostream& operator<<(std::ostream& out, const Result& r)
 {
   out << r.toString();
@@ -801,6 +805,10 @@ std::string Sort::toString() const
   return d_type->toString();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Type Sort::getType(void) const { return *d_type; }
+
 std::ostream& operator<<(std::ostream& out, const Sort& s)
 {
   out << s.toString();
@@ -942,6 +950,10 @@ Term::const_iterator Term::end() const
   return Term::const_iterator(new CVC4::Expr::const_iterator(d_expr->end()));
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr Term::getExpr(void) const { return *d_expr; }
+
 std::ostream& operator<<(std::ostream& out, const Term& t)
 {
   out << t.toString();
@@ -1029,6 +1041,10 @@ bool OpTerm::isNull() const { return d_expr->isNull(); }
 
 std::string OpTerm::toString() const { return d_expr->toString(); }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Expr OpTerm::getExpr(void) const { return *d_expr; }
+
 std::ostream& operator<<(std::ostream& out, const OpTerm& t)
 {
   out << t.toString();
@@ -1097,6 +1113,14 @@ std::string DatatypeConstructorDecl::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructor DatatypeConstructorDecl::getDatatypeConstructor(
+    void) const
+{
+  return *d_ctor;
+}
+
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeConstructorDecl& ctordecl)
 {
@@ -1146,6 +1170,10 @@ std::string DatatypeDecl::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Datatype DatatypeDecl::getDatatype(void) const { return *d_dtype; }
+
 std::ostream& operator<<(std::ostream& out,
                          const DatatypeSelectorDecl& stordecl)
 {
@@ -1171,6 +1199,14 @@ std::string DatatypeSelector::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructorArg DatatypeSelector::getDatatypeConstructorArg(
+    void) const
+{
+  return *d_stor;
+}
+
 std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
 {
   out << stor.toString();
@@ -1287,6 +1323,14 @@ std::string DatatypeConstructor::toString() const
   return ss.str();
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::DatatypeConstructor DatatypeConstructor::getDatatypeConstructor(
+    void) const
+{
+  return *d_ctor;
+}
+
 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
 {
   out << ctor.toString();
@@ -1333,6 +1377,10 @@ Datatype::const_iterator Datatype::end() const
   return Datatype::const_iterator(*d_dtype, false);
 }
 
+// !!! This is only temporarily available until the parser is fully migrated
+// to the new API. !!!
+CVC4::Datatype Datatype::getDatatype(void) const { return *d_dtype; }
+
 Datatype::const_iterator::const_iterator(const CVC4::Datatype& dtype,
                                          bool begin)
 {
@@ -1431,10 +1479,11 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 
 Solver::Solver(Options* opts)
 {
-  d_exprMgr = std::unique_ptr<ExprManager>(
-      opts == nullptr ? new ExprManager(Options()) : new ExprManager(*opts));
-  d_smtEngine = std::unique_ptr<SmtEngine>(new SmtEngine(d_exprMgr.get()));
-  d_rng = std::unique_ptr<Random>(new Random((*opts)[options::seed]));
+  Options* o = opts == nullptr ?  new Options() : opts;
+  d_exprMgr.reset(new ExprManager(*o));
+  d_smtEngine.reset(new SmtEngine(d_exprMgr.get()));
+  d_rng.reset(new Random((*o)[options::seed]));
+  if (opts == nullptr) delete o;
 }
 
 Solver::~Solver() {}
@@ -2777,5 +2826,17 @@ void Solver::setOption(const std::string& option,
   d_smtEngine->setOption(option, value);
 }
 
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
+
+/**
+ * !!! This is only temporarily available until the parser is fully migrated to
+ * the new API. !!!
+ */
+SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
+
 }  // namespace api
 }  // namespace CVC4
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 0d05c9b19..b1a1e2abd 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -56,6 +56,15 @@ class CVC4_PUBLIC Result
   friend class Solver;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param r the internal result that is to be wrapped by this result
+   * @return the Result
+   */
+  Result(const CVC4::Result& r);
+
   /**
    * Return true if query was a satisfiable checkSat() or checkSatAssuming()
    * query.
@@ -116,14 +125,11 @@ class CVC4_PUBLIC Result
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param r the internal result that is to be wrapped by this result
-   * @return the Result
-   */
-  Result(const CVC4::Result& r);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Result getResult(void) const;
 
+ private:
   /**
    * The interal result wrapped by this result.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Result is
@@ -160,6 +166,15 @@ class CVC4_PUBLIC Sort
   friend class Term;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param t the internal type that is to be wrapped by this sort
+   * @return the Sort
+   */
+  Sort(const CVC4::Type& t);
+
   /**
    * Destructor.
    */
@@ -313,14 +328,11 @@ class CVC4_PUBLIC Sort
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param t the internal type that is to be wrapped by this sort
-   * @return the Sort
-   */
-  Sort(const CVC4::Type& t);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Type getType(void) const;
 
+ private:
   /**
    * The interal type wrapped by this sort.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -361,6 +373,15 @@ class CVC4_PUBLIC Term
   friend struct TermHashFunction;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param e the internal expression that is to be wrapped by this term
+   * @return the Term
+   */
+  Term(const CVC4::Expr& e);
+
   /**
    * Constructor.
    */
@@ -545,14 +566,11 @@ class CVC4_PUBLIC Term
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param e the internal expression that is to be wrapped by this term
-   * @return the Term
-   */
-  Term(const CVC4::Expr& e);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Expr getExpr(void) const;
 
+ private:
   /**
    * The internal expression wrapped by this term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -650,6 +668,15 @@ class CVC4_PUBLIC OpTerm
    */
   OpTerm();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param e the internal expression that is to be wrapped by this term
+   * @return the Term
+   */
+  OpTerm(const CVC4::Expr& e);
+
   /**
    * Destructor.
    */
@@ -701,14 +728,11 @@ class CVC4_PUBLIC OpTerm
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param e the internal expression that is to be wrapped by this term
-   * @return the Term
-   */
-  OpTerm(const CVC4::Expr& e);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Expr getExpr(void) const;
 
+ private:
   /**
    * The internal expression wrapped by this operator term.
    * This is a shared_ptr rather than a unique_ptr to avoid overhead due to
@@ -812,6 +836,10 @@ class CVC4_PUBLIC DatatypeConstructorDecl
    */
   std::string toString() const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
+
  private:
   /**
    * The internal (intermediate) datatype constructor wrapped by this
@@ -875,6 +903,10 @@ class CVC4_PUBLIC DatatypeDecl
    */
   std::string toString() const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Datatype getDatatype(void) const;
+
  private:
   /* The internal (intermediate) datatype wrapped by this datatype
    * declaration
@@ -898,6 +930,15 @@ class CVC4_PUBLIC DatatypeSelector
    */
   DatatypeSelector();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param stor the internal datatype selector to be wrapped
+   * @return the DatatypeSelector
+   */
+  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+
   /**
    * Destructor.
    */
@@ -908,14 +949,11 @@ class CVC4_PUBLIC DatatypeSelector
    */
   std::string toString() const;
 
- private:
-  /**
-   * Constructor.
-   * @param stor the internal datatype selector to be wrapped
-   * @return the DatatypeSelector
-   */
-  DatatypeSelector(const CVC4::DatatypeConstructorArg& stor);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructorArg getDatatypeConstructorArg(void) const;
 
+ private:
   /**
    * The internal datatype selector wrapped by this datatype selector.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -938,6 +976,15 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   DatatypeConstructor();
 
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param ctor the internal datatype constructor to be wrapped
+   * @return thte DatatypeConstructor
+   */
+  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+
   /**
    * Destructor.
    */
@@ -1048,14 +1095,11 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param ctor the internal datatype constructor to be wrapped
-   * @return thte DatatypeConstructor
-   */
-  DatatypeConstructor(const CVC4::DatatypeConstructor& ctor);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::DatatypeConstructor getDatatypeConstructor(void) const;
 
+ private:
   /**
    * The internal datatype constructor wrapped by this datatype constructor.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -1073,6 +1117,15 @@ class CVC4_PUBLIC Datatype
   friend class Sort;
 
  public:
+  // !!! This constructor is only temporarily public until the parser is fully
+  // migrated to the new API. !!!
+  /**
+   * Constructor.
+   * @param dtype the internal datatype to be wrapped
+   * @return the Datatype
+   */
+  Datatype(const CVC4::Datatype& dtype);
+
   /**
    * Destructor.
    */
@@ -1181,14 +1234,11 @@ class CVC4_PUBLIC Datatype
    */
   const_iterator end() const;
 
- private:
-  /**
-   * Constructor.
-   * @param dtype the internal datatype to be wrapped
-   * @return the Datatype
-   */
-  Datatype(const CVC4::Datatype& dtype);
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  CVC4::Datatype getDatatype(void) const;
 
+ private:
   /**
    * The internal datatype wrapped by this datatype.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is
@@ -2349,6 +2399,14 @@ class CVC4_PUBLIC Solver
    */
   void setOption(const std::string& option, const std::string& value) const;
 
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  ExprManager* getExprManager(void) const;
+
+  // !!! This is only temporarily available until the parser is fully migrated
+  // to the new API. !!!
+  SmtEngine* getSmtEngine(void) const;
+
  private:
   /* Helper to convert a vector of internal types to sorts. */
   std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index ff65e944c..7944c51ce 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -22,6 +22,7 @@
 #include <iterator>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
@@ -944,42 +945,53 @@ void ValidityChecker::setUpOptions(CVC4::Options& options, const CLFlags& clflag
   }
 }
 
-ValidityChecker::ValidityChecker() :
-  d_clflags(new CLFlags()),
-  d_options(),
-  d_em(NULL),
-  d_emmc(),
-  d_reverseEmmc(),
-  d_smt(NULL),
-  d_parserContext(NULL),
-  d_exprTypeMapRemove(),
-  d_stackLevel(0),
-  d_constructors(),
-  d_selectors() {
-  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
+ValidityChecker::ValidityChecker()
+    : d_clflags(new CLFlags()),
+      d_options(),
+      d_em(NULL),
+      d_emmc(),
+      d_reverseEmmc(),
+      d_smt(NULL),
+      d_parserContext(NULL),
+      d_exprTypeMapRemove(),
+      d_stackLevel(0),
+      d_constructors(),
+      d_selectors()
+{
+  d_solver.reset(new CVC4::api::Solver(&d_options));
+  d_smt = d_solver->getSmtEngine();
+  d_em = reinterpret_cast<ExprManager*>(d_solver->getExprManager());
   s_validityCheckers[d_em] = this;
-  d_smt = new CVC4::SmtEngine(d_em);
   setUpOptions(d_options, *d_clflags);
-  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
-}
-
-ValidityChecker::ValidityChecker(const CLFlags& clflags) :
-  d_clflags(new CLFlags(clflags)),
-  d_options(),
-  d_em(NULL),
-  d_emmc(),
-  d_reverseEmmc(),
-  d_smt(NULL),
-  d_parserContext(NULL),
-  d_exprTypeMapRemove(),
-  d_stackLevel(0),
-  d_constructors(),
-  d_selectors() {
-  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
+  d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>")
+                        .withInputLanguage(CVC4::language::input::LANG_CVC4)
+                        .withStringInput("")
+                        .build();
+}
+
+ValidityChecker::ValidityChecker(const CLFlags& clflags)
+    : d_clflags(new CLFlags(clflags)),
+      d_options(),
+      d_em(NULL),
+      d_emmc(),
+      d_reverseEmmc(),
+      d_smt(NULL),
+      d_parserContext(NULL),
+      d_exprTypeMapRemove(),
+      d_stackLevel(0),
+      d_constructors(),
+      d_selectors()
+{
+  d_solver.reset(new CVC4::api::Solver(&d_options));
+  d_smt = d_solver->getSmtEngine();
+  d_em = reinterpret_cast<ExprManager*>(d_solver->getExprManager());
   s_validityCheckers[d_em] = this;
   d_smt = new CVC4::SmtEngine(d_em);
   setUpOptions(d_options, *d_clflags);
-  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
+  d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>")
+                        .withInputLanguage(CVC4::language::input::LANG_CVC4)
+                        .withStringInput("")
+                        .build();
 }
 
 ValidityChecker::~ValidityChecker() {
@@ -989,14 +1001,12 @@ ValidityChecker::~ValidityChecker() {
   }
   d_exprTypeMapRemove.clear();
   delete d_parserContext;
-  delete d_smt;
   d_emmc.clear();
   for(set<ValidityChecker*>::iterator i = d_reverseEmmc.begin(); i != d_reverseEmmc.end(); ++i) {
     (*i)->d_emmc.erase(d_em);
   }
   d_reverseEmmc.clear();
   s_validityCheckers.erase(d_em);
-  delete d_em;
   delete d_clflags;
 }
 
@@ -1609,7 +1619,11 @@ Expr ValidityChecker::exprFromString(const std::string& s, InputLanguage lang) {
     throw Exception("Unsupported language in exprFromString: " + ss.str());
   }
 
-  CVC4::parser::Parser* p = CVC4::parser::ParserBuilder(d_em, "<internal>").withStringInput(s).withInputLanguage(lang).build();
+  CVC4::parser::Parser* p =
+      CVC4::parser::ParserBuilder(d_solver.get(), "<internal>")
+          .withStringInput(s)
+          .withInputLanguage(lang)
+          .build();
   p->useDeclarationsFrom(d_parserContext);
   Expr e = p->nextExpression();
   if( e.isNull() ) {
@@ -2570,7 +2584,10 @@ void ValidityChecker::reset() {
   // reset everything, forget everything
   d_smt->reset();
   delete d_parserContext;
-  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
+  d_parserContext = CVC4::parser::ParserBuilder(d_solver.get(), "<internal>")
+                        .withInputLanguage(CVC4::language::input::LANG_CVC4)
+                        .withStringInput("")
+                        .build();
   s_typeToExpr.clear();
   s_exprToType.clear();
 }
@@ -2600,7 +2617,7 @@ void ValidityChecker::loadFile(const std::string& fileName,
   langss << lang;
   d_smt->setOption("input-language", CVC4::SExpr(langss.str()));
   d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false));
-  CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts);
+  CVC4::parser::ParserBuilder parserBuilder(d_solver.get(), fileName, opts);
   CVC4::parser::Parser* p = parserBuilder.build();
   p->useDeclarationsFrom(d_parserContext);
   doCommands(p, d_smt, opts);
@@ -2617,7 +2634,7 @@ void ValidityChecker::loadFile(std::istream& is,
   langss << lang;
   d_smt->setOption("input-language", CVC4::SExpr(langss.str()));
   d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false));
-  CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts);
+  CVC4::parser::ParserBuilder parserBuilder(d_solver.get(), "[stream]", opts);
   CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build();
   d_parserContext = p;
   p->useDeclarationsFrom(d_parserContext);
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 7120e01f2..c9bde2fa0 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -2,7 +2,7 @@
 /*! \file cvc3_compat.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Francois Bobot
+ **   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.
@@ -232,6 +232,9 @@ class CVC4_PUBLIC Context;
 class CVC4_PUBLIC Proof {};
 class CVC4_PUBLIC Theorem {};
 
+namespace api {
+class CVC4_PUBLIC Solver;
+}
 using CVC4::InputLanguage;
 using CVC4::Integer;
 using CVC4::Rational;
@@ -513,6 +516,7 @@ class CVC4_PUBLIC ValidityChecker {
 
   CLFlags* d_clflags;
   CVC4::Options d_options;
+  std::unique_ptr<CVC4::api::Solver> d_solver;
   CVC3::ExprManager* d_em;
   std::map<CVC4::ExprManager*, CVC4::ExprManagerMapCollection> d_emmc;
   std::set<ValidityChecker*> d_reverseEmmc;
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 0fd421b24..40c31de99 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -24,6 +24,7 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "main/main.h"
 #include "smt/command.h"
 
@@ -48,15 +49,29 @@ void setNoLimitCPU() {
 
 void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
 
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
-  d_exprMgr(exprMgr),
-  d_smtEngine(new SmtEngine(&exprMgr)),
-  d_options(options),
-  d_stats("driver"),
-  d_result(),
-  d_replayStream(NULL)
+CommandExecutor::CommandExecutor(api::Solver* solver, Options& options)
+    : d_solver(solver),
+      d_smtEngine(d_solver->getSmtEngine()),
+      d_options(options),
+      d_stats("driver"),
+      d_result(),
+      d_replayStream(NULL)
 {}
 
+void CommandExecutor::flushStatistics(std::ostream& out) const
+{
+  d_solver->getExprManager()->getStatistics().flushInformation(out);
+  d_smtEngine->getStatistics().flushInformation(out);
+  d_stats.flushInformation(out);
+}
+
+void CommandExecutor::safeFlushStatistics(int fd) const
+{
+  d_solver->getExprManager()->safeFlushStatistics(fd);
+  d_smtEngine->safeFlushStatistics(fd);
+  d_stats.safeFlushInformation(fd);
+}
+
 void CommandExecutor::setReplayStream(ExprStream* replayStream) {
   assert(d_replayStream == NULL);
   d_replayStream = replayStream;
@@ -92,11 +107,11 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  if(d_options.getStatistics()) {
+  if (d_options.getStatistics())
+  {
     flushStatistics(*d_options.getErr());
   }
-  delete d_smtEngine;
-  d_smtEngine = new SmtEngine(&d_exprMgr);
+  d_solver->reset();
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 31a604174..7e7202a5a 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -2,7 +2,7 @@
 /*! \file command_executor.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Morgan Deters, Tim King
+ **   Kshitij Bansal, 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.
@@ -25,6 +25,11 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+namespace api {
+class Solver;
+}
+
 namespace main {
 
 class CommandExecutor {
@@ -32,21 +37,22 @@ private:
   std::string d_lastStatistics;
 
 protected:
-  ExprManager& d_exprMgr;
-  SmtEngine* d_smtEngine;
-  Options& d_options;
-  StatisticsRegistry d_stats;
-  Result d_result;
-  ExprStream* d_replayStream;
+ api::Solver* d_solver;
+ SmtEngine* d_smtEngine;
+ Options& d_options;
+ StatisticsRegistry d_stats;
+ Result d_result;
+ ExprStream* d_replayStream;
 
 public:
-  CommandExecutor(ExprManager &exprMgr, Options &options);
-
-  virtual ~CommandExecutor() {
-    delete d_smtEngine;
-    if(d_replayStream != NULL){
-      delete d_replayStream;
-    }
+ CommandExecutor(api::Solver* solver, Options& options);
+
+ virtual ~CommandExecutor()
+ {
+   if (d_replayStream != NULL)
+   {
+     delete d_replayStream;
+   }
   }
 
   /**
@@ -63,20 +69,16 @@ public:
     return d_stats;
   }
 
-  virtual void flushStatistics(std::ostream& out) const {
-    d_exprMgr.getStatistics().flushInformation(out);
-    d_smtEngine->getStatistics().flushInformation(out);
-    d_stats.flushInformation(out);
-  }
+  /**
+   * Flushes statistics to a file descriptor.
+   */
+  virtual void flushStatistics(std::ostream& out) const;
 
   /**
-   * Flushes statistics to a file descriptor. Safe to use in a signal handler.
+   * Flushes statistics to a file descriptor.
+   * Safe to use in a signal handler.
    */
-  void safeFlushStatistics(int fd) const {
-    d_exprMgr.safeFlushStatistics(fd);
-    d_smtEngine->safeFlushStatistics(fd);
-    d_stats.safeFlushInformation(fd);
-  }
+  void safeFlushStatistics(int fd) const;
 
   static void printStatsFilterZeros(std::ostream& out,
                                     const std::string& statsString);
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f97b037eb..c29212c4f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,6 +26,7 @@
 // This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
 
+#include "api/cvc4cpp.h"
 #include "base/configuration.h"
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
@@ -200,10 +201,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
 
   // Create the expression manager using appropriate options
-  ExprManager* exprMgr;
+  std::unique_ptr<api::Solver> solver;
 # ifndef PORTFOLIO_BUILD
-  exprMgr = new ExprManager(opts);
-  pExecutor = new CommandExecutor(*exprMgr, opts);
+  solver.reset(new api::Solver(&opts));
+  pExecutor = new CommandExecutor(solver.get(), opts);
 # else
   OptionsList threadOpts;
   parseThreadSpecificOptions(threadOpts, opts);
@@ -230,19 +231,23 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     }
   }
   // pick appropriate one
-  if(useParallelExecutor) {
-    exprMgr = new ExprManager(threadOpts[0]);
-    pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
-  } else {
-    exprMgr = new ExprManager(opts);
-    pExecutor = new CommandExecutor(*exprMgr, opts);
+  if (useParallelExecutor)
+  {
+    solver.reset(&threadOpts[0]);
+    pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts);
+  }
+  else
+  {
+    solver.reset(&opts);
+    pExecutor = new CommandExecutor(solver.get(), opts);
   }
 # endif
 
   std::unique_ptr<Parser> replayParser;
-  if( opts.getReplayInputFilename() != "" ) {
+  if (opts.getReplayInputFilename() != "")
+  {
     std::string replayFilename = opts.getReplayInputFilename();
-    ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts);
+    ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts);
 
     if( replayFilename == "-") {
       if( inputFromStdin ) {
@@ -281,7 +286,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 #endif /* PORTFOLIO_BUILD */
-      InteractiveShell shell(*exprMgr);
+      InteractiveShell shell(solver.get());
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
@@ -334,7 +339,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // delete cmd;
       }
 
-      ParserBuilder parserBuilder(exprMgr, filename, opts);
+      ParserBuilder parserBuilder(solver.get(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -491,7 +496,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
       }
 
-      ParserBuilder parserBuilder(exprMgr, filename, opts);
+      ParserBuilder parserBuilder(solver.get(), filename, opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -578,7 +583,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // need to be around in that case for main() to print statistics.
   delete pTotalTime;
   delete pExecutor;
-  delete exprMgr;
 
   pTotalTime = NULL;
   pExecutor = NULL;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 2cec42fbf..aeccd3a64 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -37,6 +37,7 @@
 #  endif /* HAVE_EXT_STDIO_FILEBUF_H */
 #endif /* HAVE_LIBREADLINE */
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "options/language.h"
 #include "options/options.h"
@@ -87,13 +88,13 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBREADLINE */
 
-InteractiveShell::InteractiveShell(ExprManager& exprManager)
-    : d_options(exprManager.getOptions()),
+InteractiveShell::InteractiveShell(api::Solver* solver)
+    : d_options(solver->getExprManager()->getOptions()),
       d_in(*d_options.getIn()),
       d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options);
+  ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 203dfb766..ac52a78c4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -25,9 +25,12 @@
 namespace CVC4 {
 
 class Command;
-class ExprManager;
 class Options;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
   class Parser;
 }/* CVC4::parser namespace */
@@ -47,7 +50,7 @@ class CVC4_PUBLIC InteractiveShell
   static const unsigned s_historyLimit = 500;
 
 public:
- InteractiveShell(ExprManager& exprManager);
+ InteractiveShell(api::Solver* solver);
 
  /**
   * Close out the interactive session.
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 4da6dbb81..d9a065fd5 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -29,7 +29,6 @@ namespace CVC4 {
 
 class Command;
 class Expr;
-class ExprManager;
 
 namespace parser {
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 47124a589..182abb89b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -25,6 +25,7 @@
 #include <sstream>
 #include <unordered_set>
 
+#include "api/cvc4cpp.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
@@ -42,10 +43,12 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
-Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode,
+Parser::Parser(api::Solver* solver,
+               Input* input,
+               bool strictMode,
                bool parseOnly)
-    : d_exprManager(exprManager),
-      d_resourceManager(d_exprManager->getResourceManager()),
+    : d_solver(solver),
+      d_resourceManager(d_solver->getExprManager()->getResourceManager()),
       d_input(input),
       d_symtabAllocated(),
       d_symtab(&d_symtabAllocated),
@@ -58,7 +61,8 @@ Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode,
       d_parseOnly(parseOnly),
       d_canIncludeFile(true),
       d_logicIsForced(false),
-      d_forcedLogic() {
+      d_forcedLogic()
+{
   d_input->setParser(*this);
 }
 
@@ -72,6 +76,11 @@ Parser::~Parser() {
   delete d_input;
 }
 
+ExprManager* Parser::getExprManager() const
+{
+  return d_solver->getExprManager();
+}
+
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   checkDeclaration(name, CHECK_DECLARED, type);
   assert(isDeclared(name, type));
@@ -120,12 +129,12 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
   if(isDefinedFunction(expr)) {
     // defined functions/constants are wrapped in an APPLY so that they are
     // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions
-    expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr);
+    expr = getExprManager()->mkExpr(CVC4::kind::APPLY, expr);
   }else{
     Type te = expr.getType();
     if(te.isConstructor() && ConstructorType(te).getArity() == 0) {
       // nullary constructors have APPLY_CONSTRUCTOR kind with no children
-      expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+      expr = getExprManager()->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
     }
   }
   return expr;
@@ -210,14 +219,14 @@ Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bo
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(name, type, flags);
+  Expr expr = getExprManager()->mkVar(name, type, flags);
   defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
   return expr;
 }
 
 Expr Parser::mkBoundVar(const std::string& name, const Type& type) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
-  Expr expr = d_exprManager->mkBoundVar(name, type);
+  Expr expr = getExprManager()->mkBoundVar(name, type);
   defineVar(name, expr, false);
   return expr;
 }
@@ -228,7 +237,7 @@ Expr Parser::mkFunction(const std::string& name, const Type& type,
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(name, type, flags);
+  Expr expr = getExprManager()->mkVar(name, type, flags);
   defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
   return expr;
 }
@@ -240,7 +249,7 @@ Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
   }
   stringstream name;
   name << prefix << "_anon_" << ++d_anonymousFunctionCount;
-  return d_exprManager->mkVar(name.str(), type, flags);
+  return getExprManager()->mkVar(name.str(), type, flags);
 }
 
 std::vector<Expr> Parser::mkVars(const std::vector<std::string> names,
@@ -318,7 +327,7 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  Type type = d_exprManager->mkSort(name, flags);
+  Type type = getExprManager()->mkSort(name, flags);
   defineType(name, type);
   return type;
 }
@@ -330,7 +339,7 @@ SortConstructorType Parser::mkSortConstructor(const std::string& name,
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
   SortConstructorType type =
-      d_exprManager->mkSortConstructor(name, arity, flags);
+      getExprManager()->mkSortConstructor(name, arity, flags);
   defineType(name, vector<Type>(arity), type);
   return type;
 }
@@ -353,7 +362,7 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor(
     const std::string& name, const std::vector<Type>& params) {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  SortConstructorType unresolved = d_exprManager->mkSortConstructor(
+  SortConstructorType unresolved = getExprManager()->mkSortConstructor(
       name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
   defineType(name, params, unresolved);
   Type t = getSort(name, params);
@@ -372,7 +381,7 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
     std::vector<Datatype>& datatypes, bool doOverload) {
   try {
     std::vector<DatatypeType> types =
-        d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+        getExprManager()->mkMutualDatatypeTypes(datatypes, d_unresolved);
 
     assert(datatypes.size() == types.size());
 
@@ -467,7 +476,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts,
       // the introduced variable is internal (not parsable)
       std::stringstream ss;
       ss << "__flatten_var_" << i;
-      Expr v = d_exprManager->mkBoundVar(ss.str(), domainTypes[i]);
+      Expr v = getExprManager()->mkBoundVar(ss.str(), domainTypes[i]);
       flattenVars.push_back(v);
     }
     range = static_cast<FunctionType>(range).getRangeType();
@@ -476,7 +485,7 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts,
   {
     return range;
   }
-  return d_exprManager->mkFunctionType(sorts, range);
+  return getExprManager()->mkFunctionType(sorts, range);
 }
 
 Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range)
@@ -493,14 +502,14 @@ Type Parser::mkFlatFunctionType(std::vector<Type>& sorts, Type range)
     sorts.insert(sorts.end(), domainTypes.begin(), domainTypes.end());
     range = static_cast<FunctionType>(range).getRangeType();
   }
-  return d_exprManager->mkFunctionType(sorts, range);
+  return getExprManager()->mkFunctionType(sorts, range);
 }
 
 Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args, unsigned startIndex)
 {
   for (unsigned i = startIndex; i < args.size(); i++)
   {
-    expr = d_exprManager->mkExpr(HO_APPLY, expr, args[i]);
+    expr = getExprManager()->mkExpr(HO_APPLY, expr, args[i]);
   }
   return expr;
 }
@@ -573,8 +582,8 @@ void Parser::checkArity(Kind kind, unsigned numArgs)
     return;
   }
 
-  unsigned min = d_exprManager->minArity(kind);
-  unsigned max = d_exprManager->maxArity(kind);
+  unsigned min = getExprManager()->minArity(kind);
+  unsigned max = getExprManager()->maxArity(kind);
 
   if (numArgs < min || numArgs > max) {
     stringstream ss;
@@ -630,7 +639,7 @@ Command* Parser::nextCommand()
       dynamic_cast<QuitCommand*>(cmd) == NULL) {
     // don't count set-option commands as to not get stuck in an infinite
     // loop of resourcing out
-    const Options& options = d_exprManager->getOptions();
+    const Options& options = getExprManager()->getOptions();
     d_resourceManager->spendResource(options.getParseStep());
   }
   return cmd;
@@ -639,7 +648,7 @@ Command* Parser::nextCommand()
 Expr Parser::nextExpression()
 {
   Debug("parser") << "nextExpression()" << std::endl;
-  const Options& options = d_exprManager->getOptions();
+  const Options& options = getExprManager()->getOptions();
   d_resourceManager->spendResource(options.getParseStep());
   Expr result;
   if (!done()) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 78cbcaafb..b0519691c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -24,23 +24,25 @@
 #include <list>
 #include <cassert>
 
-#include "parser/input.h"
-#include "parser/parser_exception.h"
 #include "expr/expr.h"
-#include "expr/symbol_table.h"
-#include "expr/kind.h"
 #include "expr/expr_stream.h"
+#include "expr/kind.h"
+#include "expr/symbol_table.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
 // Forward declarations
 class BooleanType;
-class ExprManager;
 class Command;
 class FunctionType;
 class Type;
 class ResourceManager;
+namespace api {
+class Solver;
+}
 
 //for sygus gterm two-pass parsing
 class CVC4_PUBLIC SygusGTerm {
@@ -135,135 +137,137 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 class CVC4_PUBLIC Parser {
   friend class ParserBuilder;
 private:
-  /** The expression manager */
-  ExprManager *d_exprManager;
-  /** The resource manager associated with this expr manager */
-  ResourceManager *d_resourceManager;
+ /** The API Solver object. */
+ api::Solver* d_solver;
 
-  /** The input that we're parsing. */
-  Input *d_input;
+ /** The resource manager associated with this expr manager */
+ ResourceManager* d_resourceManager;
 
-  /**
-   * The declaration scope that is "owned" by this parser.  May or
-   * may not be the current declaration scope in use.
-   */
-  SymbolTable d_symtabAllocated;
+ /** The input that we're parsing. */
+ Input* d_input;
 
-  /**
-   * This current symbol table used by this parser.  Initially points
-   * to d_symtabAllocated, but can be changed (making this parser
-   * delegate its definitions and lookups to another parser).
-   * See useDeclarationsFrom().
-   */
-  SymbolTable* d_symtab;
+ /**
+  * The declaration scope that is "owned" by this parser.  May or
+  * may not be the current declaration scope in use.
+  */
+ SymbolTable d_symtabAllocated;
 
-  /**
-   * The level of the assertions in the declaration scope.  Things declared
-   * after this level are bindings from e.g. a let, a quantifier, or a
-   * lambda.
-   */
-  size_t d_assertionLevel;
+ /**
+  * This current symbol table used by this parser.  Initially points
+  * to d_symtabAllocated, but can be changed (making this parser
+  * delegate its definitions and lookups to another parser).
+  * See useDeclarationsFrom().
+  */
+ SymbolTable* d_symtab;
 
-  /**
-   * Whether we're in global declarations mode (all definitions and
-   * declarations are global).
-   */
-  bool d_globalDeclarations;
+ /**
+  * The level of the assertions in the declaration scope.  Things declared
+  * after this level are bindings from e.g. a let, a quantifier, or a
+  * lambda.
+  */
+ size_t d_assertionLevel;
 
-  /**
-   * Maintains a list of reserved symbols at the assertion level that might
-   * not occur in our symbol table.  This is necessary to e.g. support the
-   * proper behavior of the :named annotation in SMT-LIBv2 when used under
-   * a let or a quantifier, since inside a let/quant body the declaration
-   * scope is that of the let/quant body, but the defined name should be
-   * reserved at the assertion level.
-   */
-  std::set<std::string> d_reservedSymbols;
+ /**
+  * Whether we're in global declarations mode (all definitions and
+  * declarations are global).
+  */
+ bool d_globalDeclarations;
+
+ /**
+  * Maintains a list of reserved symbols at the assertion level that might
+  * not occur in our symbol table.  This is necessary to e.g. support the
+  * proper behavior of the :named annotation in SMT-LIBv2 when used under
+  * a let or a quantifier, since inside a let/quant body the declaration
+  * scope is that of the let/quant body, but the defined name should be
+  * reserved at the assertion level.
+  */
+ std::set<std::string> d_reservedSymbols;
 
-  /** How many anonymous functions we've created. */
-  size_t d_anonymousFunctionCount;
+ /** How many anonymous functions we've created. */
+ size_t d_anonymousFunctionCount;
 
-  /** Are we done */
-  bool d_done;
+ /** Are we done */
+ bool d_done;
 
-  /** Are semantic checks enabled during parsing? */
-  bool d_checksEnabled;
+ /** Are semantic checks enabled during parsing? */
+ bool d_checksEnabled;
 
-  /** Are we parsing in strict mode? */
-  bool d_strictMode;
+ /** Are we parsing in strict mode? */
+ bool d_strictMode;
 
-  /** Are we only parsing? */
-  bool d_parseOnly;
+ /** Are we only parsing? */
+ bool d_parseOnly;
 
-  /**
-   * Can we include files?  (Set to false for security purposes in
-   * e.g. the online version.)
-   */
-  bool d_canIncludeFile;
-
-  /**
-   * Whether the logic has been forced with --force-logic.
-   */
-  bool d_logicIsForced;
+ /**
+  * Can we include files?  (Set to false for security purposes in
+  * e.g. the online version.)
+  */
+ bool d_canIncludeFile;
 
-  /**
-   * The logic, if d_logicIsForced == true.
-   */
-  std::string d_forcedLogic;
+ /**
+  * Whether the logic has been forced with --force-logic.
+  */
+ bool d_logicIsForced;
 
-  /** The set of operators available in the current logic. */
-  std::set<Kind> d_logicOperators;
+ /**
+  * The logic, if d_logicIsForced == true.
+  */
+ std::string d_forcedLogic;
 
-  /** The set of attributes already warned about. */
-  std::set<std::string> d_attributesWarnedAbout;
+ /** The set of operators available in the current logic. */
+ std::set<Kind> d_logicOperators;
 
-  /**
-   * The current set of unresolved types.  We can get by with this NOT
-   * being on the scope, because we can only have one DATATYPE
-   * definition going on at one time.  This is a bit hackish; we
-   * depend on mkMutualDatatypeTypes() to check everything and clear
-   * this out.
-   */
-  std::set<Type> d_unresolved;
+ /** The set of attributes already warned about. */
+ std::set<std::string> d_attributesWarnedAbout;
 
-  /**
-   * "Preemption commands": extra commands implied by subterms that
-   * should be issued before the currently-being-parsed command is
-   * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
-   *
-   * Owns the memory of the Commands in the queue.
-   */
-  std::list<Command*> d_commandQueue;
+ /**
+  * The current set of unresolved types.  We can get by with this NOT
+  * being on the scope, because we can only have one DATATYPE
+  * definition going on at one time.  This is a bit hackish; we
+  * depend on mkMutualDatatypeTypes() to check everything and clear
+  * this out.
+  */
+ std::set<Type> d_unresolved;
+
+ /**
+  * "Preemption commands": extra commands implied by subterms that
+  * should be issued before the currently-being-parsed command is
+  * issued.  Used to support SMT-LIBv2 ":named" attribute on terms.
+  *
+  * Owns the memory of the Commands in the queue.
+  */
+ std::list<Command*> d_commandQueue;
 
-  /** Lookup a symbol in the given namespace (as specified by the type). 
-   * Only returns a symbol if it is not overloaded, returns null otherwise.
-   */
-  Expr getSymbol(const std::string& var_name, SymbolType type);
+ /** Lookup a symbol in the given namespace (as specified by the type).
+  * Only returns a symbol if it is not overloaded, returns null otherwise.
+  */
+ Expr getSymbol(const std::string& var_name, SymbolType type);
 
 protected:
-  /**
-   * Create a parser state.
-   *
-   * @attention The parser takes "ownership" of the given
-   * input and will delete it on destruction.
-   *
-   * @param exprManager the expression manager to use when creating expressions
-   * @param input the parser input
-   * @param strictMode whether to incorporate strict(er) compliance checks
-   * @param parseOnly whether we are parsing only (and therefore certain checks
-   * need not be performed, like those about unimplemented features, @see
-   * unimplementedFeature())
-   */
-  Parser(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+ /**
+  * Create a parser state.
+  *
+  * @attention The parser takes "ownership" of the given
+  * input and will delete it on destruction.
+  *
+  * @param the solver API object
+  * @param input the parser input
+  * @param strictMode whether to incorporate strict(er) compliance checks
+  * @param parseOnly whether we are parsing only (and therefore certain checks
+  * need not be performed, like those about unimplemented features, @see
+  * unimplementedFeature())
+  */
+ Parser(api::Solver* solver,
+        Input* input,
+        bool strictMode = false,
+        bool parseOnly = false);
 
 public:
 
   virtual ~Parser();
 
   /** Get the associated <code>ExprManager</code>. */
-  inline ExprManager* getExprManager() const {
-    return d_exprManager;
-  }
+  ExprManager* getExprManager() const;
 
   /** Get the associated input. */
   inline Input* getInput() const {
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 4505c4f86..95a3a7840 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -2,7 +2,7 @@
 /*! \file parser_builder.cpp
  ** \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.
@@ -21,10 +21,11 @@
 
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
+#include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
-#include "options/options.h"
 #include "smt1/smt1.h"
 #include "smt2/smt2.h"
 #include "tptp/tptp.h"
@@ -32,29 +33,28 @@
 namespace CVC4 {
 namespace parser {
 
-ParserBuilder::ParserBuilder(ExprManager* exprManager,
-                             const std::string& filename) :
-  d_filename(filename),
-  d_exprManager(exprManager) {
-  init(exprManager, filename);
+ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename)
+    : d_filename(filename), d_solver(solver)
+{
+  init(solver, filename);
 }
 
-ParserBuilder::ParserBuilder(ExprManager* exprManager,
+ParserBuilder::ParserBuilder(api::Solver* solver,
                              const std::string& filename,
-                             const Options& options) :
-  d_filename(filename),
-  d_exprManager(exprManager) {
-  init(exprManager, filename);
+                             const Options& options)
+    : d_filename(filename), d_solver(solver)
+{
+  init(solver, filename);
   withOptions(options);
 }
 
-void ParserBuilder::init(ExprManager* exprManager,
-                         const std::string& filename) {
+void ParserBuilder::init(api::Solver* solver, const std::string& filename)
+{
   d_inputType = FILE_INPUT;
   d_lang = language::input::LANG_AUTO;
   d_filename = filename;
   d_streamInput = NULL;
-  d_exprManager = exprManager;
+  d_solver = solver;
   d_checksEnabled = true;
   d_strictMode = false;
   d_canIncludeFile = true;
@@ -87,26 +87,27 @@ Parser* ParserBuilder::build()
   assert(input != NULL);
 
   Parser* parser = NULL;
-  switch(d_lang) {
-  case language::input::LANG_SMTLIB_V1:
-    parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
-  case language::input::LANG_SYGUS:
-    parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
-  case language::input::LANG_TPTP:
-    parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
-  default:
-    if (language::isInputLang_smt2(d_lang))
-    {
-      parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
-    }
-    else
-    {
-      parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
-    }
-    break;
+  switch (d_lang)
+  {
+    case language::input::LANG_SMTLIB_V1:
+      parser = new Smt1(d_solver, input, d_strictMode, d_parseOnly);
+      break;
+    case language::input::LANG_SYGUS:
+      parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+      break;
+    case language::input::LANG_TPTP:
+      parser = new Tptp(d_solver, input, d_strictMode, d_parseOnly);
+      break;
+    default:
+      if (language::isInputLang_smt2(d_lang))
+      {
+        parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+      }
+      else
+      {
+        parser = new Parser(d_solver, input, d_strictMode, d_parseOnly);
+      }
+      break;
   }
 
   if( d_checksEnabled ) {
@@ -133,8 +134,9 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withExprManager(ExprManager* exprManager) {
-  d_exprManager = exprManager;
+ParserBuilder& ParserBuilder::withSolver(api::Solver* solver)
+{
+  d_solver = solver;
   return *this;
 }
 
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index c4c75aae5..3e14d715a 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -2,7 +2,7 @@
 /*! \file parser_builder.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.
@@ -26,9 +26,12 @@
 
 namespace CVC4 {
 
-class ExprManager;
 class Options;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
 
 class Parser;
@@ -61,8 +64,8 @@ class CVC4_PUBLIC ParserBuilder {
   /** The stream input, if any. */
   std::istream* d_streamInput;
 
-  /** The expression manager */
-  ExprManager* d_exprManager;
+  /** The API Solver object. */
+  api::Solver* d_solver;
 
   /** Should semantic checks be enabled during parsing? */
   bool d_checksEnabled;
@@ -86,14 +89,14 @@ class CVC4_PUBLIC ParserBuilder {
   std::string d_forcedLogic;
 
   /** Initialize this parser builder */
-  void init(ExprManager* exprManager, const std::string& filename);
-
-public:
+  void init(api::Solver* solver, const std::string& filename);
 
-  /** Create a parser builder using the given ExprManager and filename. */
-  ParserBuilder(ExprManager* exprManager, const std::string& filename);
+ public:
+  /** Create a parser builder using the given Solver and filename. */
+  ParserBuilder(api::Solver* solver, const std::string& filename);
 
-  ParserBuilder(ExprManager* exprManager, const std::string& filename,
+  ParserBuilder(api::Solver* solver,
+                const std::string& filename,
                 const Options& options);
 
   /** Build the parser, using the current settings. */
@@ -102,8 +105,8 @@ public:
   /** Should semantic checks be enabled in the parser? (Default: yes) */
   ParserBuilder& withChecks(bool flag = true);
 
-  /** Set the ExprManager to use with the parser. */
-  ParserBuilder& withExprManager(ExprManager* exprManager);
+  /** Set the Solver to use with the parser. */
+  ParserBuilder& withSolver(api::Solver* solver);
 
   /** Set the parser to read a file for its input. (Default) */
   ParserBuilder& withFileInput();
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 87da44c0e..544c6e85c 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -14,9 +14,10 @@
 
 #include "parser/smt1/smt1.h"
 
+#include "api/cvc4cpp.h"
 #include "expr/type.h"
-#include "smt/command.h"
 #include "parser/parser.h"
+#include "smt/command.h"
 
 namespace CVC4 {
 namespace parser {
@@ -70,9 +71,9 @@ Smt1::Logic Smt1::toLogic(const std::string& name) {
   return logicMap[name];
 }
 
-Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode,
-           bool parseOnly)
-    : Parser(exprManager, input, strictMode, parseOnly), d_logic(UNSET) {
+Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
+    : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET)
+{
   // Boolean symbols are always defined
   addOperator(kind::AND);
   addOperator(kind::EQUAL);
@@ -81,7 +82,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode,
   addOperator(kind::NOT);
   addOperator(kind::OR);
   addOperator(kind::XOR);
-
 }
 
 void Smt1::addArithmeticOperators() {
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h
index 42b6a4157..fe177d21e 100644
--- a/src/parser/smt1/smt1.h
+++ b/src/parser/smt1/smt1.h
@@ -2,7 +2,7 @@
 /*! \file smt1.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.
@@ -26,6 +26,10 @@ namespace CVC4 {
 
 class SExpr;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
 
 class Smt1 : public Parser {
@@ -93,7 +97,10 @@ private:
   Logic d_logic;
 
 protected:
-  Smt1(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+ Smt1(api::Solver* solver,
+      Input* input,
+      bool strictMode = false,
+      bool parseOnly = false);
 
 public:
   /**
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a0cc750b3..0a93beb2e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -15,6 +15,7 @@
  **/
 #include "parser/smt2/smt2.h"
 
+#include "api/cvc4cpp.h"
 #include "expr/type.h"
 #include "options/options.h"
 #include "parser/antlr_input.h"
@@ -34,10 +35,11 @@
 namespace CVC4 {
 namespace parser {
 
-Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
-  Parser(exprManager,input,strictMode,parseOnly),
-  d_logicSet(false) {
-  if( !strictModeEnabled() ) {
+Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
+    : Parser(solver, input, strictMode, parseOnly), d_logicSet(false)
+{
+  if (!strictModeEnabled())
+  {
     addTheory(Smt2::THEORY_CORE);
   }
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c9b224d39..64a957402 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -34,6 +34,10 @@ namespace CVC4 {
 
 class SExpr;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
 
 class Smt2 : public Parser {
@@ -69,7 +73,10 @@ private:
   std::map< Expr, bool > d_sygusVarPrimed;
 
 protected:
-  Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+ Smt2(api::Solver* solver,
+      Input* input,
+      bool strictMode = false,
+      bool parseOnly = false);
 
 public:
   /**
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 0228fdeff..ee313a202 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -20,6 +20,7 @@
 #include <algorithm>
 #include <set>
 
+#include "api/cvc4cpp.h"
 #include "expr/type.h"
 #include "parser/parser.h"
 
@@ -30,11 +31,9 @@
 namespace CVC4 {
 namespace parser {
 
-Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode,
-           bool parseOnly)
-    : Parser(exprManager, input, strictMode, parseOnly),
-      d_cnf(false),
-      d_fof(false) {
+Tptp::Tptp(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
+    : Parser(solver, input, strictMode, parseOnly), d_cnf(false), d_fof(false)
+{
   addTheory(Tptp::THEORY_CORE);
 
   /* Try to find TPTP dir */
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 3ce9668e0..eb5532247 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -30,6 +30,11 @@
 #include "util/hash.h"
 
 namespace CVC4 {
+
+namespace api {
+class Solver;
+}
+
 namespace parser {
 
 class Tptp : public Parser {
@@ -81,7 +86,9 @@ class Tptp : public Parser {
   bool hasConjecture() const { return d_hasConjecture; }
 
  protected:
-  Tptp(ExprManager* exprManager, Input* input, bool strictMode = false,
+  Tptp(api::Solver* solver,
+       Input* input,
+       bool strictMode = false,
        bool parseOnly = false);
 
  public:
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