summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/main/Makefile.am8
-rw-r--r--src/main/interactive_shell.cpp111
-rw-r--r--src/main/interactive_shell.h52
-rw-r--r--src/main/main.cpp38
-rw-r--r--src/parser/antlr_input.h10
-rw-r--r--src/parser/antlr_input_imports.cpp17
-rw-r--r--src/parser/input.h9
-rw-r--r--src/parser/parser.h9
-rw-r--r--src/parser/parser_builder.cpp38
9 files changed, 226 insertions, 66 deletions
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 <iostream>
+
+#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 <iostream>
+#include <string>
+
+#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<CommandSequence*>(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 <em>only</me> 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback