From: Tim King <taking@cs.nyu.edu>
Date: Wed, 30 Mar 2011 17:32:50 +0000 (+0000)
Subject: Moved the constructor for Options out of the header and into the cpp. For people... 
X-Git-Tag: cvc5-1.0.0~8627
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb058369e08b17c51d0267c87890edd8c41255c2;p=cvc5.git

Moved the constructor for Options out of the header and into the cpp. For people who fiddle with default values set by the Options constructor, this will require significantly less recompiling.
---

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 94d479166..1b73361c3 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -40,6 +40,45 @@ using namespace CVC4;
 
 namespace CVC4 {
 
+#ifdef CVC4_DEBUG
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
+#else /* CVC4_DEBUG */
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
+#endif /* CVC4_DEBUG */
+
+#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+
+Options::Options() :
+  binary_name(),
+  statistics(false),
+  in(&std::cin),
+  out(&std::cout),
+  err(&std::cerr),
+  verbosity(0),
+  inputLanguage(language::input::LANG_AUTO),
+  uf_implementation(MORGAN),
+  parseOnly(false),
+  semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
+  theoryRegistration(true),
+  memoryMap(false),
+  strictParsing(false),
+  lazyDefinitionExpansion(false),
+  interactive(false),
+  interactiveSetByUser(false),
+  segvNoSpin(false),
+  produceModels(false),
+  produceAssignments(false),
+  typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
+  earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
+  incrementalSolving(false),
+  pivotRule(MINIMUM)
+{
+}
+
 static const string optionsDescription = "\
    --lang | -L            force input language (default is `auto'; see --lang help)\n\
    --version | -V         identify this CVC4 binary\n\
@@ -447,4 +486,8 @@ throw(OptionException) {
 
 bool Options::rewriteArithEqualities = false;
 
+
+#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
 }/* CVC4 namespace */
diff --git a/src/util/options.h b/src/util/options.h
index 2ddc8224f..32ce77a64 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -21,18 +21,6 @@
 #ifndef __CVC4__OPTIONS_H
 #define __CVC4__OPTIONS_H
 
-#ifdef CVC4_DEBUG
-#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
-#else /* CVC4_DEBUG */
-#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
-#endif /* CVC4_DEBUG */
-
-#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
-
 #include <iostream>
 #include <string>
 
@@ -134,34 +122,9 @@ struct CVC4_PUBLIC Options {
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;
 
-  Options() :
-    binary_name(),
-    statistics(false),
-    in(&std::cin),
-    out(&std::cout),
-    err(&std::cerr),
-    verbosity(0),
-    inputLanguage(language::input::LANG_AUTO),
-    uf_implementation(MORGAN),
-    parseOnly(false),
-    semanticChecks(DO_SEMANTIC_CHECKS_BY_DEFAULT),
-    theoryRegistration(true),
-    memoryMap(false),
-    strictParsing(false),
-    lazyDefinitionExpansion(false),
-    interactive(false),
-    interactiveSetByUser(false),
-    segvNoSpin(false),
-    produceModels(false),
-    produceAssignments(false),
-    typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
-    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
-    incrementalSolving(false),
-    pivotRule(MINIMUM)
-    {
-  }
+  Options();
 
-  /** 
+  /**
    * Get a description of the command-line flags accepted by
    * parseOptions.  The returned string will be escaped so that it is
    * suitable as an argument to printf. */
@@ -195,7 +158,4 @@ inline std::ostream& operator<<(std::ostream& out,
 
 }/* CVC4 namespace */
 
-#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
-#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
-
 #endif /* __CVC4__OPTIONS_H */