Adding --parse-only option

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 0c041b05ea9c483c648e92029acb7475da524486..ff9957c5c779140ba943308822f9f3efa07894c4 100644 (file)
--- 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 bb38c6147623748b8032ad52a72374792a3a2a49..d0ad72fc456dadfe430a4a7f1e38171ec4bfd968 100644 (file)
--- 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 f13c4aebe864fbec3eded6c449a984c0e0708486..79b906d8804e8116df71891731d5a5f1240c1705 100644 (file)
--- 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 f3bc52d34ef2503aac4871375ec7c5d3d27c5486..0a1766c09b7a64d8e0400ae302835d9c2b83f166 100644 (file)
--- 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 */