diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-05 22:24:09 +0000 |
commit | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (patch) | |
tree | 8db12e260b24978bbbed3363846f6daf7c0da04f /src/main | |
parent | 5e2f381b26d683691d9a040589536dc39c5831e0 (diff) |
parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/getopt.cpp | 16 | ||||
-rw-r--r-- | src/main/main.cpp | 30 |
2 files changed, 33 insertions, 13 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 08bcbaa7c..4af882aa1 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -70,7 +70,9 @@ enum OptionValue { STRICT_PARSING, DEFAULT_EXPR_DEPTH, PRINT_EXPR_TYPES, - UF_THEORY + UF_THEORY, + INTERACTIVE, + NO_INTERACTIVE };/* enum OptionValue */ /** @@ -117,6 +119,8 @@ static struct option cmdlineOptions[] = { { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH }, { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES }, { "uf" , required_argument, NULL, UF_THEORY }, + { "interactive", no_argument , NULL, INTERACTIVE }, + { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -268,6 +272,16 @@ throw(OptionException) { } break; + case INTERACTIVE: + opts->interactive = true; + opts->interactiveSetByUser = true; + break; + + case NO_INTERACTIVE: + opts->interactive = false; + opts->interactiveSetByUser = true; + break; + case SHOW_CONFIG: fputs(Configuration::about().c_str(), stdout); printf("\n"); diff --git a/src/main/main.cpp b/src/main/main.cpp index f0c04e5f6..4f261378d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -110,20 +110,25 @@ int runCvc4(int argc, char* argv[]) { throw Exception("Too many input files specified."); } + // If no file supplied we will read from standard input + const bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + + // if we're reading from stdin, default to interactive mode + if(!options.interactiveSetByUser) { + options.interactive = inputFromStdin; + } + // Create the expression manager ExprManager exprMgr; // Create the SmtEngine SmtEngine smt(&exprMgr, &options); - // If no file supplied we read from standard input - bool inputFromStdin = - firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); - // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; - ReferenceStat< const char* > s_statFilename("filename",filename); + ReferenceStat< const char* > s_statFilename("filename", filename); StatisticsRegistry::registerStat(&s_statFilename); if(options.lang == parser::LANG_AUTO) { @@ -180,6 +185,9 @@ int runCvc4(int argc, char* argv[]) { // Parse and execute commands until we are done Command* cmd; + if( options.interactive ) { + // cout << "CVC4> " << flush; + } while((cmd = parser->nextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); @@ -238,21 +246,19 @@ void doCommand(SmtEngine& smt, Command* cmd) { cout << "Invoking: " << *cmd << endl; } - cmd->invoke(&smt); + if(options.verbosity >= 0) { + cmd->invoke(&smt, cout); + } else { + cmd->invoke(&smt); + } QueryCommand *qc = dynamic_cast<QueryCommand*>(cmd); if(qc != NULL) { lastResult = qc->getResult(); - if(options.verbosity >= 0) { - cout << lastResult << endl; - } } else { CheckSatCommand *csc = dynamic_cast<CheckSatCommand*>(cmd); if(csc != NULL) { lastResult = csc->getResult(); - if(options.verbosity >= 0) { - cout << lastResult << endl; - } } } } |