Plug solver API object into parser. (#2240)

11 files changed, 237 insertions, 198 deletions

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: