Made use of minimizing solver an option (ssplitting_total_model off),…

… which is default. This should make SSplitter use the total model as computed by the SAT solver.

Saturation/SSplitter.cpp

@@ -63,16 +63,16 @@ void SSplittingBranchSelector::init()
 
   switch(_parent.getOptions().satSolver()){
     case Options::BUFFERED_VAMPIRE:
-      _solver = new MinimizingSolver(new BufferedSolver(new TWLSolver(_parent.getOptions(),true)));
+      _solver = new BufferedSolver(new TWLSolver(_parent.getOptions(),true));
       break;
     case Options::VAMPIRE:  
-      _solver = new MinimizingSolver(new TWLSolver(_parent.getOptions(), true));
+      _solver = new TWLSolver(_parent.getOptions(), true);
       break;
     case Options::BUFFERED_LINGELING: 
-      _solver = new MinimizingSolver(new BufferedSolver(new LingelingInterfacing(_parent.getOptions(), true)));
+      _solver = new BufferedSolver(new LingelingInterfacing(_parent.getOptions(), true));
       break;
     case Options::LINGELING: 
-      _solver = new MinimizingSolver(new LingelingInterfacing(_parent.getOptions(), true));
+      _solver = new LingelingInterfacing(_parent.getOptions(), true);
       break;
     case Options::BUFFERED_MINISAT:
       _solver = new MinimizingSolver(new BufferedSolver(new MinisatInterfacing(_parent.getOptions(),true)));
@@ -84,6 +84,10 @@ void SSplittingBranchSelector::init()
       ASSERTION_VIOLATION_REP(_parent.getOptions().satSolver());
   }
 
+  if(!_parent.getOptions().ssplittingTotalModel()){
+    _solver = new MinimizingSolver(_solver.release());
+  }
+
 #if DEBUG_MIN_SOLVER
   _solver = new Test::CheckedSatSolver(_solver.release());
 #endif

Shell/Options.cpp

@@ -996,6 +996,7 @@ Options::Options ()
   _ssplittingFlushPeriod(0),
   _ssplittingFlushQuotient(1.5f),
   _ssplittingNonsplittableComponents(SSNS_KNOWN),
+  _ssplittingTotalModel(false),
   _statistics(STATISTICS_FULL),
   _superpositionFromVariables(true),
   _symbolPrecedence(BY_ARITY),