summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
Diffstat (limited to 'src/main')
-rw-r--r--src/main/getopt.cpp10
-rw-r--r--src/main/main.cpp4
-rw-r--r--src/main/usage.h1
3 files changed, 12 insertions, 3 deletions
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 0c041b05e..ff9957c5c 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -57,7 +57,8 @@ enum OptionValue {
CNF = 256, /* no clash with char options */
SMTCOMP,
STATS,
- SEGV_NOSPIN
+ SEGV_NOSPIN,
+ PARSE_ONLY
};/* enum OptionValue */
// FIXME add a comment here describing the option array
@@ -72,7 +73,8 @@ static struct option cmdlineOptions[] = {
{ "cnf" , required_argument, NULL, CNF },
{ "smtcomp" , no_argument , NULL, SMTCOMP },
{ "stats" , no_argument , NULL, STATS },
- { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }
+ { "segv-nospin", no_argument , NULL, SEGV_NOSPIN },
+ { "parse-only" , no_argument , NULL, PARSE_ONLY }
};/* if you add things to the above, please remember to update usage.h! */
/** Full argv[0] */
@@ -170,6 +172,10 @@ throw(OptionException) {
opts->lang = Parser::LANG_SMTLIB;
break;
+ case PARSE_ONLY:
+ opts->parseOnly = true;
+ break;
+
case '?':
throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'");
diff --git a/src/main/main.cpp b/src/main/main.cpp
index bb38c6147..d0ad72fc4 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -114,7 +114,9 @@ int main(int argc, char *argv[]) {
// Parse and execute commands until we are done
Command* cmd;
while((cmd = parser->parseNextCommand())) {
- doCommand(smt, cmd);
+ if( !options.parseOnly ) {
+ doCommand(smt, cmd);
+ }
delete cmd;
}
diff --git a/src/main/usage.h b/src/main/usage.h
index f13c4aebe..79b906d88 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -36,6 +36,7 @@ CVC4 options:\n\
--smtcomp competition mode (very quiet)\n\
--stats give statistics on exit\n\
--segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\
+ --parse-only exit after parsing input\n\
";
}/* CVC4::main namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback