#include "interactive_shell.h"
#include "expr/command.h"
+#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
namespace CVC4 {
+const string InteractiveShell::INPUT_FILENAME = "<shell>";
+
Command* InteractiveShell::readCommand() {
/* Don't do anything if the input is closed. */
if( d_in.eof() ) {
}
}
- Parser *parser =
- d_parserBuilder
- .withStringInput(input)
- .withStateFrom(d_lastParser)
- .build();
+ d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME));
+ // Parser *parser =
+ // d_parserBuilder
+ // .withStringInput(input)
+ // .withStateFrom(d_lastParser)
+ // .build();
/* There may be more than one command in the input. Build up a
sequence. */
CommandSequence *cmd_seq = new CommandSequence();
Command *cmd;
- while( (cmd = parser->nextCommand()) ) {
+ while( (cmd = d_parser->nextCommand()) ) {
cmd_seq->addCommand(cmd);
}
- delete d_lastParser;
- d_lastParser = parser;
+ // if( d_lastParser ) {
+ // delete d_lastParser;
+ // }
+ // d_lastParser = parser;
return cmd_seq;
}
#include <string>
#include "parser/parser_builder.h"
+#include "util/language.h"
#include "util/options.h"
namespace CVC4 {
class CVC4_PUBLIC InteractiveShell {
std::istream& d_in;
std::ostream& d_out;
- ParserBuilder d_parserBuilder;
- Parser* d_lastParser;
+ Parser* d_parser;
+ const InputLanguage d_language;
+
+ static const std::string INPUT_FILENAME;
public:
- InteractiveShell(ParserBuilder& parserBuilder,
+ InteractiveShell(ExprManager& exprManager,
const Options& options) :
d_in(*options.in),
d_out(*options.out),
- d_parserBuilder(parserBuilder),
- d_lastParser(NULL) {
+ d_language(options.inputLanguage) {
+ ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
+ /* Create parser with bogus input. */
+ d_parser = parserBuilder.withStringInput("").build();
}
/** Read a command from the interactive shell. This will read as
Warning.getStream() << Expr::setlanguage(language);
}
- ParserBuilder parserBuilder =
- ParserBuilder(exprMgr, filename, options);
-
- if( inputFromStdin ) {
- parserBuilder.withStreamInput(cin);
- }
// Parse and execute commands until we are done
Command* cmd;
if( options.interactive ) {
- InteractiveShell shell(parserBuilder,options);
+ InteractiveShell shell(exprMgr,options);
while((cmd = shell.readCommand())) {
doCommand(smt,cmd);
delete cmd;
}
} else {
+ ParserBuilder parserBuilder =
+ ParserBuilder(exprMgr, filename, options);
+
+ if( inputFromStdin ) {
+ parserBuilder.withStreamInput(cin);
+ }
+
Parser *parser = parserBuilder.build();
while((cmd = parser->nextCommand())) {
doCommand(smt, cmd);
Input(const Input& input) { Unimplemented("Copy constructor for Input."); }
Input& operator=(const Input& input) { Unimplemented("operator= for Input."); }
+public:
+
/** Create an input for the given file.
*
* @param lang the input language
const std::string& name)
throw (InputStreamException, AssertionException);
-public:
/** Destructor. Frees the input stream and closes the input. */
virtual ~Input();
/** Retrieve the input stream for this parser. */
InputStream *getInputStream();
- /** Parse a command from
- * the input by invoking the implementation-specific parsing method. Returns
+ /** Parse a command from the input by invoking the
+ * implementation-specific parsing method. Returns
* <code>NULL</code> if there is no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
virtual void parseError(const std::string& msg)
throw (ParserException, AssertionException) = 0;
- /** Parse an
- * expression from the input by invoking the implementation-specific
- * parsing method. Returns a null <code>Expr</code> if there is no
- * expression there to parse.
+ /** Parse an expression from the input by invoking the
+ * implementation-specific parsing method. Returns a null
+ * <code>Expr</code> if there is no expression there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
return d_input;
}
+ /** Deletes and replaces the current parser input. */
+ void setInput(Input* input) {
+ delete d_input;
+ d_input = 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.
namespace parser {
-/*class FileInputBuilder : public InputBuilder {
- bool d_useMmap;
-public:
- FileInputBuilder(InputLanguage lang, const std::string& filename, bool useMmap) :
- InputBuilder(lang,filename),
- d_useMmap(useMmap) {
- }
- ParserBuilder& useMmap();
-
- Input& build() {
- return Input::newFileInput(d_lang,d_name,d_useMmap);
- }
-};
-
-class StringInputBuilder : public InputBuilder {
- std::string d_input;
-public:
- StringInputBuilder(InputLanguage lang, const std::string& input, const std::string& name) :
- InputBuilder(lang,name),
- d_input(input) {
- }
-
- Input& build() {
- return Input::newStringInput(lang,input,name);
- }
-};*/
-
-ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename)// :
- // d_inputType(FILE_INPUT),
- // d_lang(language::input::LANG_AUTO),
- : d_filename(filename),
- // d_streamInput(NULL),
- d_exprManager(exprManager)
- // d_checksEnabled(true),
- // d_strictMode(false),
- // d_mmap(false)
-{
+ParserBuilder::ParserBuilder(ExprManager& exprManager,
+ const std::string& filename) :
+ d_filename(filename),
+ d_exprManager(exprManager) {
init(exprManager,filename);
}
- ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename, const Options& options) :
+ParserBuilder::ParserBuilder(ExprManager& exprManager,
+ const std::string& filename,
+ const Options& options) :
d_filename(filename),
- d_exprManager(exprManager)
-{
+ d_exprManager(exprManager) {
init(exprManager,filename);
withOptions(options);
}
- void ParserBuilder::init(ExprManager& exprManager, const std::string& filename) {
+void ParserBuilder::init(ExprManager& exprManager,
+ const std::string& filename) {
d_inputType = FILE_INPUT;
d_lang = language::input::LANG_AUTO;
d_filename = filename;
d_streamInput = NULL;
d_exprManager = exprManager;
- d_parserToUseForState = NULL;
d_checksEnabled = true;
d_strictMode = false;
d_mmap = false;
}
-Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) {
+Parser *ParserBuilder::build()
+ throw (InputStreamException,AssertionException) {
Input *input = NULL;
switch( d_inputType ) {
case FILE_INPUT:
parser->disableChecks();
}
- if( d_parserToUseForState != NULL ) {
- parser->d_declScope = d_parserToUseForState->d_declScope;
- parser->d_logicOperators = d_parserToUseForState->d_logicOperators;
- }
-
return parser;
}
.withStrictMode(options.strictParsing);
}
-ParserBuilder& ParserBuilder::withStateFrom(const Parser* parser) {
- d_parserToUseForState = parser;
- return *this;
-}
-
ParserBuilder& ParserBuilder::withStrictMode(bool flag) {
d_strictMode = flag;
return *this;
namespace parser {
-/*
-class InputBuilder {
-protected:
- InputLanguage d_lang;
- std::string d_name;
-public:
- InputBuilder(InputLanguage lang, const std::string& name) :
- d_lang(lang),
- d_name(name) {
- }
- virtual Input& build() = 0;
-};
-*/
-
class Parser;
/**
/** The expression manager */
ExprManager& d_exprManager;
- /** Parser to derive the initial state from. */
- const Parser* d_parserToUseForState;
-
/** Should semantic checks be enabled during parsing? */
bool d_checksEnabled;
/** Derive settings from the given options. */
ParserBuilder& withOptions(const Options& options);
- /** Copy the state (e.g., variable and type declaration) from
- * an existing parser. If <code>parser</code> is <code>NULL</code>,
- * the default initial state will be used. */
- ParserBuilder& withStateFrom(const Parser* parser);
-
/** Should the parser use strict mode? (Default: no) */
ParserBuilder& withStrictMode(bool flag = true);
projects / cvc5.git / commitdiff