diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/cvc.h | 3 | ||||
-rw-r--r-- | src/parser/parser.cpp | 8 | ||||
-rw-r--r-- | src/parser/parser.h | 11 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 79 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 58 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 3 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 1 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 5 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 1 |
9 files changed, 21 insertions, 148 deletions
diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index e14f1bc7a..e20e041cc 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -38,10 +38,9 @@ class Cvc : public Parser protected: Cvc(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false) - : Parser(solver, sm, input, strictMode, parseOnly) + : Parser(solver, sm, strictMode, parseOnly) { } }; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 31f8517cd..f3a0d5c83 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -39,15 +39,13 @@ namespace parser { Parser::Parser(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : d_input(input), - d_symman(sm), + : d_symman(sm), d_symtab(sm->getSymbolTable()), d_assertionLevel(0), d_anonymousFunctionCount(0), - d_done(false), + d_done(true), d_checksEnabled(true), d_strictMode(strictMode), d_parseOnly(parseOnly), @@ -56,7 +54,6 @@ Parser::Parser(api::Solver* solver, d_forcedLogic(), d_solver(solver) { - d_input->setParser(*this); } Parser::~Parser() { @@ -66,7 +63,6 @@ Parser::~Parser() { delete command; } d_commandQueue.clear(); - delete d_input; } api::Solver* Parser::getSolver() const { return d_solver; } diff --git a/src/parser/parser.h b/src/parser/parser.h index 42baf98cd..b127221d7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -19,6 +19,7 @@ #define CVC5__PARSER__PARSER_H #include <list> +#include <memory> #include <set> #include <string> @@ -107,7 +108,7 @@ class CVC5_EXPORT Parser private: /** The input that we're parsing. */ - Input* d_input; + std::unique_ptr<Input> d_input; /** * Reference to the symbol manager, which manages the symbol table used by @@ -207,7 +208,6 @@ protected: */ Parser(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); @@ -219,17 +219,14 @@ public: api::Solver* getSolver() const; /** Get the associated input. */ - inline Input* getInput() const { - return d_input; - } + Input* getInput() const { return d_input.get(); } /** Get unresolved sorts */ inline std::set<api::Sort>& getUnresolvedSorts() { return d_unresolved; } /** Deletes and replaces the current parser input. */ void setInput(Input* input) { - delete d_input; - d_input = input; + d_input.reset(input); d_input->setParser(*this); d_done = false; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 220edb9d5..26a867f95 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -31,38 +31,29 @@ namespace cvc5 { namespace parser { -ParserBuilder::ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const std::string& filename) - : d_filename(filename), d_solver(solver), d_symman(sm) +ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm) + : d_solver(solver), d_symman(sm) { - init(solver, sm, filename); + init(solver, sm); } ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm, - const std::string& filename, const Options& options) - : d_filename(filename), d_solver(solver), d_symman(sm) + : d_solver(solver), d_symman(sm) { - init(solver, sm, filename); + init(solver, sm); withOptions(options); } -void ParserBuilder::init(api::Solver* solver, - SymbolManager* sm, - const std::string& filename) +void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) { - d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; - d_filename = filename; - d_streamInput = NULL; d_solver = solver; d_symman = sm; d_checksEnabled = true; d_strictMode = false; d_canIncludeFile = true; - d_mmap = false; d_parseOnly = false; d_logicIsForced = false; d_forcedLogic = ""; @@ -70,39 +61,23 @@ void ParserBuilder::init(api::Solver* solver, Parser* ParserBuilder::build() { - Input* input = NULL; - switch( d_inputType ) { - case FILE_INPUT: - input = Input::newFileInput(d_lang, d_filename, d_mmap); - break; - case STREAM_INPUT: - Assert(d_streamInput != NULL); - input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); - break; - case STRING_INPUT: - input = Input::newStringInput(d_lang, d_stringInput, d_filename); - break; - } - - Assert(input != NULL); - Parser* parser = NULL; switch (d_lang) { case language::input::LANG_SYGUS_V2: - parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); break; case language::input::LANG_TPTP: - parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly); break; default: if (language::isInputLang_smt2(d_lang)) { - parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); } else { - parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly); } break; } @@ -131,32 +106,11 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withSolver(api::Solver* solver) -{ - d_solver = solver; - return *this; -} - -ParserBuilder& ParserBuilder::withFileInput() { - d_inputType = FILE_INPUT; - return *this; -} - -ParserBuilder& ParserBuilder::withFilename(const std::string& filename) { - d_filename = filename; - return *this; -} - ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { d_lang = lang; return *this; } -ParserBuilder& ParserBuilder::withMmap(bool flag) { - d_mmap = flag; - return *this; -} - ParserBuilder& ParserBuilder::withParseOnly(bool flag) { d_parseOnly = flag; return *this; @@ -166,7 +120,6 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) { ParserBuilder& retval = *this; retval = retval.withInputLanguage(options.getInputLanguage()) - .withMmap(options.getMemoryMap()) .withChecks(options.getSemanticChecks()) .withStrictMode(options.getStrictParsing()) .withParseOnly(options.getParseOnly()) @@ -194,17 +147,5 @@ ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) { return *this; } -ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { - d_inputType = STREAM_INPUT; - d_streamInput = &input; - return *this; -} - -ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { - d_inputType = STRING_INPUT; - d_stringInput = input; - return *this; -} - } // namespace parser } // namespace cvc5 diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index b43da3548..992ca408a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -44,27 +44,9 @@ class Parser; */ class CVC5_EXPORT ParserBuilder { - enum InputType { - FILE_INPUT, - STREAM_INPUT, - STRING_INPUT - }; - - /** The input type. */ - InputType d_inputType; - /** The input language */ InputLanguage d_lang; - /** The file name (may not exist) */ - std::string d_filename; - - /** The string input, if any. */ - std::string d_stringInput; - - /** The stream input, if any. */ - std::istream* d_streamInput; - /** The API Solver object. */ api::Solver* d_solver; @@ -80,9 +62,6 @@ class CVC5_EXPORT ParserBuilder /** Should we allow include-file commands? */ bool d_canIncludeFile; - /** Should we memory-map a file input? */ - bool d_mmap; - /** Are we parsing only? */ bool d_parseOnly; @@ -93,19 +72,14 @@ class CVC5_EXPORT ParserBuilder std::string d_forcedLogic; /** Initialize this parser builder */ - void init(api::Solver* solver, - SymbolManager* sm, - const std::string& filename); + void init(api::Solver* solver, SymbolManager* sm); public: /** Create a parser builder using the given Solver and filename. */ - ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const std::string& filename); + ParserBuilder(api::Solver* solver, SymbolManager* sm); ParserBuilder(api::Solver* solver, SymbolManager* sm, - const std::string& filename, const Options& options); /** Build the parser, using the current settings. */ @@ -114,20 +88,6 @@ class CVC5_EXPORT ParserBuilder /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); - /** 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(); - - /** - * Set the filename for use by the parser. If file input is used, - * this file will be opened and read by the parser. Otherwise, the - * filename string (possibly a non-existent path) will only be used - * in error messages. - */ - ParserBuilder& withFilename(const std::string& filename); - /** * Set the input language to be used by the parser. * @@ -136,14 +96,6 @@ class CVC5_EXPORT ParserBuilder ParserBuilder& withInputLanguage(InputLanguage lang); /** - * Should the parser memory-map its input? This is only relevant if - * the parser will have a file input. - * - * (Default: no) - */ - ParserBuilder& withMmap(bool flag = true); - - /** * Are we only parsing, or doing something with the resulting * commands and expressions? This setting affects whether the * parser will raise certain errors about unimplemented features, @@ -173,12 +125,6 @@ class CVC5_EXPORT ParserBuilder */ ParserBuilder& withIncludeFile(bool flag = true); - /** Set the parser to use the given stream for its input. */ - ParserBuilder& withStreamInput(std::istream& input); - - /** Set the parser to use the given string for its input. */ - ParserBuilder& withStringInput(const std::string& input); - /** Set the parser to use the given logic string. */ ParserBuilder& withForcedLogic(const std::string& logic); }; /* class ParserBuilder */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2f19d16f0..a91c713d6 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -31,10 +31,9 @@ namespace parser { Smt2::Smt2(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : Parser(solver, sm, input, strictMode, parseOnly), + : Parser(solver, sm, strictMode, parseOnly), d_logicSet(false), d_seenSetLogic(false) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e28ef955c..2dd4bf663 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -66,7 +66,6 @@ class Smt2 : public Parser protected: Smt2(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 01b4c1165..156f2e1e6 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -34,12 +34,9 @@ namespace parser { Tptp::Tptp(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : Parser(solver, sm, input, strictMode, parseOnly), - d_cnf(false), - d_fof(false) + : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false) { addTheory(Tptp::THEORY_CORE); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 0be74c79d..964c0bdfb 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -90,7 +90,6 @@ class Tptp : public Parser { protected: Tptp(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); |