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, 6 insertions, 11 deletions

diff --git a/src/util/options.h b/src/util/options.h
index d6c4e9009..57b20c47f 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -18,6 +18,7 @@
 
 #include <iostream>
 #include "parser/parser.h"
+#include "smt/cnf_conversion.h"
 
 namespace CVC4 {
 
@@ -38,26 +39,20 @@ struct Options {
   /* with 3, the solver is slowed down by all the scrolling */
   int verbosity;
 
-  /** The input language option */
-  enum InputLanguage {
-    /** The SMTLIB input language */
-    LANG_SMTLIB,
-    /** The CVC4 input language */
-    LANG_CVC4,
-    /** Auto-detect the language */
-    LANG_AUTO
-  };
-
   /** The input language */
   parser::Parser::InputLanguage lang;
 
+  /** The CNF conversion */
+  CVC4::CnfConversion d_cnfConversion;
+
   Options() : binary_name(),
               smtcomp_mode(false),
               statistics(false),
               out(0),
               err(0),
               verbosity(0),
-              lang(parser::Parser::LANG_AUTO)
+              lang(parser::Parser::LANG_AUTO),
+              d_cnfConversion(CVC4::CNF_DIRECT_EXPONENTIAL)
   {}
 };/* struct Options */