Plug solver API object into parser. (#2240)

2 files changed, 12 insertions, 6 deletions

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: