diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-08-08 19:21:47 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-08 19:21:47 -0700 |
commit | 91d85704313de6be9fd382833f5cedd39e24a6fa (patch) | |
tree | 057adfdad9d586428482d9bd58e9c8124bddc47b /src/parser/parser_builder.cpp | |
parent | b4d4006d08a32b107257b0edaba95679d0b0c65b (diff) |
Plug solver API object into parser. (#2240)
Diffstat (limited to 'src/parser/parser_builder.cpp')
-rw-r--r-- | src/parser/parser_builder.cpp | 76 |
1 files changed, 39 insertions, 37 deletions
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; } |