summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/parser/parser.cpp27
-rw-r--r--src/parser/parser.h9
-rw-r--r--src/parser/parser_builder.h12
3 files changed, 8 insertions, 40 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8512f55eb..697e86fe2 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -69,33 +69,6 @@ Parser::~Parser() {
d_commandQueue.clear();
}
-std::unique_ptr<InputParser> Parser::parseFile(const std::string& fname,
- bool useMmap)
-{
- d_input = Input::newFileInput(d_lang, fname, useMmap);
- d_input->setParser(*this);
- d_done = false;
- return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
-std::unique_ptr<InputParser> Parser::parseStream(const std::string& name,
- std::istream& stream)
-{
- d_input = Input::newStreamInput(d_lang, stream, name);
- d_input->setParser(*this);
- d_done = false;
- return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
-std::unique_ptr<InputParser> Parser::parseString(const std::string& name,
- const std::string& str)
-{
- d_input = Input::newStringInput(d_lang, str, name);
- d_input->setParser(*this);
- d_done = false;
- return std::unique_ptr<InputParser>(new InputParser(this, d_input));
-}
-
api::Solver* Parser::getSolver() const { return d_solver; }
api::Term Parser::getSymbol(const std::string& name, SymbolType type)
diff --git a/src/parser/parser.h b/src/parser/parser.h
index a22b24a0c..a7674ea63 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -252,11 +252,18 @@ class CVC5_EXPORT Parser
api::Solver* getSolver() const;
/** Get the associated input. */
- 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) {
+ d_input.reset(input);
+ d_input->setParser(*this);
+ d_done = false;
+ }
+
/**
* Check if we are done -- either the end of input has been reached, or some
* error has been encountered.
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index ee918ae43..992ca408a 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -44,18 +44,6 @@ class Parser;
*/
class CVC5_EXPORT ParserBuilder
{
-<<<<<<< HEAD
-=======
- enum InputType {
- FILE_INPUT,
- STREAM_INPUT,
- STRING_INPUT
- };
-
- /** The input type. */
- InputType d_inputType;
-
->>>>>>> 81404ddfc (Always parse streams with line buffer)
/** The input language */
InputLanguage d_lang;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback