fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)

1 files changed, 24 insertions, 1 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 123bc3204..388e58a3b 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -46,9 +46,16 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt | smtlib  SMT-LIB format\n\
 ";
 
+static const char cnf_help[] = "\
+CNF conversions currently supported as arguments to the --cnf option:\n\
+  direct  put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\
+  var     variable-introduction method (new vars, no exp. blow up in # clauses)\n\
+";
+
 // FIXME add a comment here describing the purpose of this
 enum OptionValue {
-  SMTCOMP = 256, /* no clash with char options */
+  CNF = 256, /* no clash with char options */
+  SMTCOMP,
   STATS
 };/* enum OptionValue */
 
@@ -61,6 +68,7 @@ static struct option cmdlineOptions[] = {
   { "quiet"  , no_argument      , NULL, 'q'     },
   { "lang"   , required_argument, NULL, 'L'     },
   { "debug"  , required_argument, NULL, 'd'     },
+  { "cnf"    , required_argument, NULL, CNF     },
   { "smtcomp", no_argument      , NULL, SMTCOMP },
   { "stats"  , no_argument      , NULL, STATS   }
 };/* if you add things to the above, please remember to update usage.h! */
@@ -117,6 +125,21 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti
       fputs(lang_help, stdout);
       exit(1);
 
+    case CNF:
+      if(!strcmp(optarg, "direct")) {
+        opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL;
+        break;
+      } else if(!strcmp(optarg, "var")) {
+        opts->d_cnfConversion = CNF_VAR_INTRODUCTION;
+        break;
+      } else if(strcmp(optarg, "help")) {
+        throw OptionException(string("unknown CNF conversion for --cnf: `") +
+                              optarg + "'.  Try --cnf help.");
+      }
+
+      fputs(cnf_help, stdout);
+      exit(1);
+
     case 'd':
       Debug.on(optarg);
       /* fall-through */