Plug solver API object into parser. (#2240)

2 files changed, 14 insertions, 5 deletions

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:
   /**