From: Christopher L. Conway Date: Wed, 20 Oct 2010 20:41:03 +0000 (+0000) Subject: Adding support for interactive mode X-Git-Tag: cvc5-1.0.0~8798 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=93e8bc35db891c6041f9690366be933433a0ad52;p=cvc5.git Adding support for interactive mode --- diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 3cd062158..b6cdbb1f4 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -6,11 +6,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas bin_PROGRAMS = cvc4 cvc4_SOURCES = \ - main.cpp \ getopt.cpp \ - util.cpp \ + interactive_shell.h \ + interactive_shell.cpp \ main.h \ - usage.h + main.cpp \ + usage.h \ + util.cpp cvc4_LDADD = \ ../parser/libcvc4parser.la \ diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp new file mode 100644 index 000000000..7af72ed2d --- /dev/null +++ b/src/main/interactive_shell.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file interactive_shell.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Interactive shell for CVC4 + **/ + +#include + +#include "interactive_shell.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace std; + +namespace CVC4 { + +Command* InteractiveShell::readCommand() { + /* Don't do anything if the input is closed. */ + if( d_in.eof() ) { + return NULL; + } + + /* If something's wrong with the input, there's nothing we can do. */ + if( !d_in.good() ) { + throw ParserException("Interactive input broken."); + } + + string input; + + /* Prompt the user for input. */ + d_out << "CVC4> " << flush; + while(true) { + stringbuf sb; + string line; + + /* Read a line */ + d_in.get(sb,'\n'); + line = sb.str(); + // cout << "Input was '" << input << "'" << endl << flush; + + /* If we hit EOF, we're done. */ + if( d_in.eof() ) { + input += line; + break; + } + + /* Check for failure */ + if( d_in.fail() ) { + /* This should only happen if the input line was empty. */ + Assert( line.empty() ); + d_in.clear(); + } + + /* Extract the newline delimiter from the stream too */ + int c = d_in.get(); + Assert( c == '\n' ); + + // cout << "Next char is '" << (char)c << "'" << endl << flush; + + /* Strip trailing whitespace. */ + int n = line.length() - 1; + while( !line.empty() && isspace(line[n]) ) { + line.erase(n,1); + n--; + } + + input += line; + + /* If the last char was a backslash, continue on the next line. */ + if( !line.empty() && line[n] == '\\' ) { + n = input.length() - 1; + Assert( input[n] == '\\' ); + input[n] = '\n'; + d_out << "... > " << flush; + } else { + /* No continuation, we're done. */ + //cout << "Leaving input loop." << endl << flush; + break; + } + } + + Parser *parser = + d_parserBuilder + .withStringInput(input) + .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()) ) { + cmd_seq->addCommand(cmd); + } + + delete parser; + return cmd_seq; +} + +} // CVC4 namespace diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h new file mode 100644 index 000000000..6bd9db295 --- /dev/null +++ b/src/main/interactive_shell.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file interactive_shell.h + ** \verbatim + ** Original author: cconway + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Interactive shell for CVC4 + **/ + +#ifndef __CVC4__INTERACTIVE_SHELL_H +#define __CVC4__INTERACTIVE_SHELL_H + +#include +#include + +#include "parser/parser_builder.h" + +namespace CVC4 { + + class Command; + + using namespace parser; + +class InteractiveShell { + std::istream& d_in; + std::ostream& d_out; + ParserBuilder d_parserBuilder; + +public: + InteractiveShell(std::istream& in, + std::ostream& out, + ParserBuilder& parserBuilder) : + d_in(in), + d_out(out), + d_parserBuilder(parserBuilder) { + } + + /** Read a command from the interactive shell. This will read as + many lines as necessary to parse a well-formed command. */ + Command *readCommand(); +}; + +} // CVC4 namespace + +#endif // __CVC4__INTERACTIVE_SHELL_H diff --git a/src/main/main.cpp b/src/main/main.cpp index d879e81df..2f524c3f6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -24,9 +24,11 @@ #include "cvc4autoconfig.h" #include "main.h" +#include "interactive_shell.h" #include "usage.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "parser/parser_exception.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" @@ -119,9 +121,13 @@ int runCvc4(int argc, char* argv[]) { firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); // if we're reading from stdin, default to interactive mode - if(!options.interactiveSetByUser) { - options.interactive = inputFromStdin; - } + // [chris 10/20/10] The expected behavior of interactive is + // different from the expected behavior of file input from + // stdin, due to EOL escapes in interactive mode + + // if(!options.interactiveSetByUser) { + // options.interactive = inputFromStdin; + // } // Create the expression manager ExprManager exprMgr(options.earlyTypeChecking); @@ -193,18 +199,22 @@ int runCvc4(int argc, char* argv[]) { parserBuilder.withStreamInput(cin); } - Parser *parser = parserBuilder.build(); - // Parse and execute commands until we are done Command* cmd; if( options.interactive ) { - // cout << "CVC4> " << flush; - } - while((cmd = parser->nextCommand())) { - if( !options.parseOnly ) { + InteractiveShell shell(cin,cout,parserBuilder); + while((cmd = shell.readCommand())) { + doCommand(smt,cmd); + delete cmd; + } + } else { + Parser *parser = parserBuilder.build(); + while((cmd = parser->nextCommand())) { doCommand(smt, cmd); + delete cmd; } - delete cmd; + // Remove the parser + delete parser; } string result = smt.getInfo(":status").getValue(); @@ -224,9 +234,6 @@ int runCvc4(int argc, char* argv[]) { exit(returnValue); #endif - // Remove the parser - delete parser; - ReferenceStat< Result > s_statSatResult("sat/unsat", result); StatisticsRegistry::registerStat(&s_statSatResult); @@ -240,7 +247,12 @@ int runCvc4(int argc, char* argv[]) { return returnValue; } +/** Executes a command. Deletes the command after execution. */ void doCommand(SmtEngine& smt, Command* cmd) { + if( options.parseOnly ) { + return; + } + CommandSequence *seq = dynamic_cast(cmd); if(seq != NULL) { for(CommandSequence::iterator subcmd = seq->begin(); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index e55e07efd..d86a18004 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -180,6 +180,8 @@ public: /** Get a bitvector constant from the text of the number and the size token */ static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size); + std::string getUnparsedText(); + protected: /** Create an input. This input takes ownership of the given input stream, * and will delete it at destruction time. @@ -210,6 +212,14 @@ protected: virtual void setParser(Parser& parser); }; +inline std::string AntlrInput::getUnparsedText() { + const char *base = (const char *)d_antlr3InputStream->data; + const char *cur = (const char *)d_antlr3InputStream->nextChar; + + return std::string(cur, d_antlr3InputStream->sizeBuf - (cur - base)); +} + + inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { ANTLR3_MARKER start = token->getStartIndex(token); ANTLR3_MARKER end = token->getStopIndex(token); diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index a1ebee523..2805d518a 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -56,6 +56,7 @@ #include "antlr_input.h" #include "parser.h" +#include "parser_exception.h" #include "util/Assert.h" using namespace std; @@ -89,6 +90,14 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; stringstream ss; + // Dig the CVC4 objects out of the ANTLR3 mess + pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); + AlwaysAssert(antlr3Parser!=NULL); + Parser *parser = (Parser*)(antlr3Parser->super); + AlwaysAssert(parser!=NULL); + AntlrInput *input = (AntlrInput*) parser->getInput() ; + AlwaysAssert(input!=NULL); + // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; @@ -252,14 +261,6 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { break; } - // Now get ready to throw an exception - pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(antlr3Parser!=NULL); - Parser *parser = (Parser*)(antlr3Parser->super); - AlwaysAssert(parser!=NULL); - AntlrInput *input = (AntlrInput*) parser->getInput() ; - AlwaysAssert(input!=NULL); - // Call the error display routine input->parseError(ss.str()); } diff --git a/src/parser/input.h b/src/parser/input.h index 1a90a4191..7cfafe429 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -47,7 +47,7 @@ public: virtual ~InputStreamException() throw() { } }; -/** Wrapper around an ANTLR3 input stream. */ +/** Wrapper around an input stream. */ class InputStream { /** The name of this input stream. */ @@ -93,7 +93,7 @@ class CVC4_PUBLIC Input { /** The input stream. */ InputStream *d_inputStream; - /* Since we own d_tokenStream and it needs to be freed, we need to prevent + /* Since we own d_inputStream and it needs to be freed, we need to prevent * copy construction and assignment. */ Input(const Input& input) { Unimplemented("Copy constructor for Input."); } @@ -134,9 +134,12 @@ class CVC4_PUBLIC Input { public: - /** Destructor. Frees the token stream and closes the input. */ + /** Destructor. Frees the input stream and closes the input. */ virtual ~Input(); + /** Retrieve the remaining text in this input. */ + virtual std::string getUnparsedText() = 0; + protected: /** Create an input. diff --git a/src/parser/parser.h b/src/parser/parser.h index 4d1e64176..280bd3c97 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -160,12 +160,6 @@ public: return d_input; } - /** Set the declaration scope manager for this input. NOTE: This should only be - * called before parsing begins. Otherwise, previous declarations will be lost. */ -/* inline void setDeclarationScope(DeclarationScope declScope) { - d_declScope = declScope; - }*/ - /** * Check if we are done -- either the end of input has been reached, or some * error has been encountered. @@ -189,7 +183,8 @@ public: /** Enable strict parsing, according to the language standards. */ void enableStrictMode() { d_strictMode = true; } - /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */ + /** Disable strict parsing. Allows certain syntactic infelicities to + pass without comment. */ void disableStrictMode() { d_strictMode = false; } bool strictModeEnabled() { return d_strictMode; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index f53d7cc9c..dcc052c3a 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -84,46 +84,20 @@ Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { default: Unreachable(); } + + Parser *parser = NULL; switch(d_lang) { case language::input::LANG_SMTLIB: - return new Smt(&d_exprManager, input, d_strictMode); + parser = new Smt(&d_exprManager, input, d_strictMode); case language::input::LANG_SMTLIB_V2: - return new Smt2(&d_exprManager, input, d_strictMode); + parser = new Smt2(&d_exprManager, input, d_strictMode); default: - return new Parser(&d_exprManager, input, d_strictMode); + parser = new Parser(&d_exprManager, input, d_strictMode); } -} - -/*ParserBuilder& ParserBuilder::disableChecks() { - d_checksEnabled = false; - return *this; -} -ParserBuilder& ParserBuilder::disableMmap() { - d_mmap = false; - return *this; -} - -ParserBuilder& ParserBuilder::disableStrictMode() { - d_strictMode = false; - return *this; + return parser; } -ParserBuilder& ParserBuilder::enableChecks() { - d_checksEnabled = true; - return *this; -} - -ParserBuilder& ParserBuilder::enableMmap() { - d_mmap = true; - return *this; -} - -ParserBuilder& ParserBuilder::enableStrictMode() { - d_strictMode = true; - return *this; -}*/ - ParserBuilder& ParserBuilder::withChecks(bool flag) { d_checksEnabled = flag; return *this;