Adding --parse-only option

4 files changed, 16 insertions, 4 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 */
diff --git a/src/util/options.h b/src/util/options.h
index f3bc52d34..0a1766c09 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -45,6 +45,8 @@ struct Options {
   /** The CNF conversion */
   CVC4::CnfConversion d_cnfConversion;
 
+  bool parseOnly;
+
   Options() : binary_name(),
               smtcomp_mode(false),
               statistics(false),
@@ -52,7 +54,8 @@ struct Options {
               err(0),
               verbosity(0),
               lang(parser::Parser::LANG_AUTO),
-              d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION)
+              d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION),
+              parseOnly(false)
   {}
 };/* struct Options */