1 files changed, 15 insertions, 12 deletions
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();