Plug solver API object into parser. (#2240)

2 files changed, 31 insertions, 27 deletions

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;