summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/cvc.h3
-rw-r--r--src/parser/parser.cpp8
-rw-r--r--src/parser/parser.h11
-rw-r--r--src/parser/parser_builder.cpp79
-rw-r--r--src/parser/parser_builder.h58
-rw-r--r--src/parser/smt2/smt2.cpp3
-rw-r--r--src/parser/smt2/smt2.h1
-rw-r--r--src/parser/tptp/tptp.cpp5
-rw-r--r--src/parser/tptp/tptp.h1
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback