adding total model option

ModelWriter · Oct 6, 2014 · 3c89359 · 3c89359
1 parent eaef0d4
commit 3c89359
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/Shell/Options.cpp b/Shell/Options.cpp
@@ -296,6 +296,7 @@ const char* Options::Constants::_optionNames[] = {
   "ssplitting_flush_period",
   "ssplitting_flush_quotient",
   "ssplitting_nonsplittable_components",
+  "ssplitting_total_model",
   "statistics",
   "superposition_from_variables",
   "symbol_precedence",
@@ -478,6 +479,7 @@ int Options::Constants::shortNameIndexes[] = {
   SSPLITTING_FLUSH_PERIOD,
   SSPLITTING_FLUSH_QUOTIENT,
   SSPLITTING_NONSPLITTABLE_COMPONENTS,
+  SSPLITTING_TOTAL_MODEL,
   SINE_TOLERANCE,
   SIMULATED_TIME_LIMIT,
 
@@ -1699,6 +1701,9 @@ void Options::set(const char* name,const char* value, int index)
     case SSPLITTING_NONSPLITTABLE_COMPONENTS:
       _ssplittingNonsplittableComponents = (SSplittingNonsplittableComponents)Constants::sSplittingNonsplittableComponentsValues.find(value);
       return;
+    case SSPLITTING_TOTAL_MODEL:
+      _ssplittingTotalModel = onOffToBool(value,name);
+      return;
 
     case STATISTICS:
       _statistics = (Statistics)Constants::statisticsValues.find(value);

diff --git a/Shell/Options.hpp b/Shell/Options.hpp
@@ -230,6 +230,7 @@ class Options
     SSPLITTING_FLUSH_PERIOD,
     SSPLITTING_FLUSH_QUOTIENT,
     SSPLITTING_NONSPLITTABLE_COMPONENTS,
+    SSPLITTING_TOTAL_MODEL,
 
     STATISTICS,
     SUPERPOSITION_FROM_VARIABLES,
@@ -808,6 +809,7 @@ class Options
   float ssplittingFlushQuotient() const { return _ssplittingFlushQuotient; }
   bool ssplittingEagerRemoval() const { return _ssplittingEagerRemoval; }
   bool ssplittingCongruenceClosure() const { return _ssplittingCongruenceClosure; }
+  bool ssplittingTotalModel() const { return _ssplittingTotalModel; }
 
   void setProof(Proof p) { _proof = p; }
   bool bpEquivalentVariableRemoval() const { return _equivalentVariableRemoval; }
@@ -1028,6 +1030,7 @@ class Options
   unsigned _ssplittingFlushPeriod;
   float _ssplittingFlushQuotient;
   SSplittingNonsplittableComponents _ssplittingNonsplittableComponents;
+  bool _ssplittingTotalModel;
   Statistics _statistics;
   bool _superpositionFromVariables;
   SymbolPrecedence _symbolPrecedence;