diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-20 20:41:03 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-10-20 20:41:03 +0000 |
commit | 93e8bc35db891c6041f9690366be933433a0ad52 (patch) | |
tree | e946c0824d6d91c44ecc97a627411e5d6c334ea9 /src/main/main.cpp | |
parent | daad722774087de1cf35714868d3762b3ea7cb21 (diff) |
Adding support for interactive mode
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r-- | src/main/main.cpp | 38 |
1 files changed, 25 insertions, 13 deletions
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(); |