From b24c3943ac3b643034913705352223e5b8c2eccc Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 6 May 2015 15:00:58 -0400
Subject: [PATCH] refactor(opensmt/smtsolvers/CoreSMTSolver.C): clean up
 duplicate code

---
 src/opensmt/smtsolvers/CoreSMTSolver.C | 79 ++++++++++----------------
 1 file changed, 30 insertions(+), 49 deletions(-)

diff --git a/src/opensmt/smtsolvers/CoreSMTSolver.C b/src/opensmt/smtsolvers/CoreSMTSolver.C
index c5d529fc0..60e37cc98 100644
--- a/src/opensmt/smtsolvers/CoreSMTSolver.C
+++ b/src/opensmt/smtsolvers/CoreSMTSolver.C
@@ -575,7 +575,7 @@ void CoreSMTSolver::cancelUntilVarTempDone( )
     vec< Lit > conflicting;
     int        max_decision_level;
     theory_handler->getConflict( conflicting, max_decision_level );
-  } 
+  }
 }
 
 //=================================================================================================
@@ -611,9 +611,9 @@ Lit CoreSMTSolver::pickBranchLit(int polarity_mode, double random_var_freq)
       Lit sugg = heuristic.getSuggestion( );
       if(var(sugg) != var_Undef){
         DREAL_LOG_DEBUG << "CoreSMTSolver::pickBranchLit() Heuristic Suggested Decision: "
-			<< sign(sugg) << " " << theory_handler->varToEnode(var(sugg))
-			<< " activity = " << activity[var(sugg)]
-			<< endl;
+                        << sign(sugg) << " " << theory_handler->varToEnode(var(sugg))
+                        << " activity = " << activity[var(sugg)]
+                        << endl;
       }
       else{
         DREAL_LOG_DEBUG << "CoreSMTSolver::pickBranchLit() Heuristic Suggested Decision: var_Undef" << endl;
@@ -659,7 +659,7 @@ Lit CoreSMTSolver::pickBranchLit(int polarity_mode, double random_var_freq)
       if(next != var_Undef){
         DREAL_LOG_DEBUG << "CoreSMTSolver::pickBranchLit() Activity Decision: "
                         << sign << " " << theory_handler->varToEnode(next)
-			<< " activity = " << activity[next]
+                        << " activity = " << activity[next]
                         << endl;
       }
                  return next == var_Undef ? lit_Undef : Lit(next, sign);
@@ -1749,54 +1749,35 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
         bool isSAT = false;
         if(config.nra_short_sat){
           //check if SAT, even if not all literals are assigned
-          isSAT = true;
-          for (int c = 0; c < nClauses(); c++) {
-            if (!satisfied(*clauses[c])) {
-              isSAT = false;
-              break;
-            }
-          }
+          isSAT = entailment();
 
-	  //Filter variables that don't need assignment
-	  filterUnassigned();
+          //Filter variables that don't need assignment
+          filterUnassigned();
 
           if( isSAT ){
             DREAL_LOG_DEBUG << "CoreSMTSolver::search() Found Model after # decisions " << decisions << endl;
-            //first_model_found = true;
             next = lit_Undef;
-          }
-          else{
+          } else {
             DREAL_LOG_DEBUG << "CoreSMTSolver::search() not SAT yet" << endl;
           }
-	  
-	  if(DREAL_LOG_DEBUG_IS_ON){
-	    DREAL_LOG_DEBUG << "Model is:";
-	    printCurrentAssignment(std::cout);
-	  }
 
+          if(DREAL_LOG_DEBUG_IS_ON){
+            DREAL_LOG_DEBUG << "Model is:";
+            printCurrentAssignment(std::cout);
+          }
         }
 
         if (next == lit_Undef){
-          if ((!config.nra_short_sat) || (!entailment())) {
-	    if( !isSAT ){       
-        	// New variable decision:
-        		DREAL_LOG_INFO << "Pick branch on a lit: " << endl;
-        		decisions++;
-        		next = pickBranchLit(polarity_mode, random_var_freq);
-	    }
-        	} else {
-	    if( !isSAT ){	      
-        	// New variable decision:
-        		DREAL_LOG_INFO << "Pick branch on a lit: " << endl;
-        		decisions++;
-        		next = pickBranchLit(polarity_mode, random_var_freq);
-	    } else {
- 
-        		// SAT formula is satisfiable
-        		next = lit_Undef;
-        		DREAL_LOG_INFO << "Found Model after # decisions " << decisions << endl;
-	    }
-        	}
+          if( !isSAT ){
+            // New variable decision:
+            DREAL_LOG_INFO << "Pick branch on a lit: " << endl;
+            decisions++;
+            next = pickBranchLit(polarity_mode, random_var_freq);
+          } else {
+            // SAT formula is satisfiable
+            next = lit_Undef;
+            DREAL_LOG_INFO << "Found Model after # decisions " << decisions << endl;
+          }
 
           // Complete Call
           if ( next == lit_Undef )
@@ -1827,8 +1808,8 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
             assert( res == 1 );
 
             if (config.nra_short_sat) {
-            	// the problem is satisfiable as res = 1 at this point
-	      if ( res == 1 ) return l_True;
+              // the problem is satisfiable as res = 1 at this point
+              return l_True;
             }
             // Otherwise we still have to make sure that
             // splitting on demand did not add any new variable
@@ -1840,12 +1821,12 @@ lbool CoreSMTSolver::search(int nof_conflicts, int nof_learnts)
             // Model found:
             DREAL_LOG_DEBUG << "CoreSMTSolver::search() Found Model after # decisions "
                             << decisions << endl;
-	    if(DREAL_LOG_DEBUG_IS_ON){
-	      DREAL_LOG_DEBUG << "Model is:";
-	      printCurrentAssignment(std::cout);
-	    }
+            if(DREAL_LOG_DEBUG_IS_ON){
+              DREAL_LOG_DEBUG << "Model is:";
+              printCurrentAssignment(std::cout);
+            }
             return l_True;
-	  }
+          }
         }
 
         // Increase decision level and enqueue 'next'