refactor(opensmt): cleanup whitespace

- no trailing whitespace - no tab. replace a hard-tab with 8 spaces
soonhokong · May 7, 2015 · c06eab2 · c06eab2
1 parent 854c4fb
commit c06eab2
Show file tree

Hide file tree

Showing 12 changed files with 634 additions and 634 deletions.
diff --git a/src/opensmt/api/OpenSMTContext.C b/src/opensmt/api/OpenSMTContext.C
@@ -815,14 +815,14 @@ void OpenSMTContext::PrintResult( const lbool & result, const lbool & config_sta
 #endif
     if (config.produce_stats){
       for( auto t : getEgraphP()->getTSolvers()){
-	dreal::nra_solver* nra = dynamic_cast<dreal::nra_solver*>(t);
-	if(nra && config.nra_output_num_nodes){
-	  out << "nodes: " << solver.decisions  << " " << config.icp_decisions() 
-	      << endl;
-	} 
-	if(nra && config.nra_model){
-	  solver.printCurrentAssignment(config.nra_model_out, true);  
-	}
+        dreal::nra_solver* nra = dynamic_cast<dreal::nra_solver*>(t);
+        if(nra && config.nra_output_num_nodes){
+          out << "nodes: " << solver.decisions  << " " << config.icp_decisions()
+              << endl;
+        }
+        if(nra && config.nra_model){
+          solver.printCurrentAssignment(config.nra_model_out, true);
+        }
       }
     }
 

diff --git a/src/opensmt/egraph/Enode.C b/src/opensmt/egraph/Enode.C
@@ -329,7 +329,7 @@ void Enode::print_infix(ostream & os, lbool polarity, string const & variable_po
             os << "(" << r << ")";
         } else {
             // Fixed Notation
-	  os << "(" << name << ")";
+          os << "(" << name << ")";
         }
         fesetround(old_rnd);
     } else if (isTerm()) {

diff --git a/src/opensmt/heuristics/heuristic.cpp b/src/opensmt/heuristics/heuristic.cpp
@@ -40,18 +40,18 @@ namespace dreal{
   }
 
   void heuristic::initialize(SMTConfig &, Egraph &, THandler*,
-			     vec<Lit> *, vec<int> *)  {
+                             vec<Lit> *, vec<int> *)  {
   }
 
   void heuristic::inform(Enode * ){
   }
 
-  void heuristic::backtrack(){   
+  void heuristic::backtrack(){
   }
 
   Lit heuristic::getSuggestion(){
   DREAL_LOG_INFO << "heuristic::getSuggestion()";
- 
+
   if(!m_is_initialized)
     return lit_Undef;
 
@@ -101,7 +101,7 @@ namespace dreal{
 
       DREAL_LOG_INFO << " -- LEVEL " << level << " (" << indx_low << ", " << indx_high << ") -- ";
       for (int i = indx_low; i < indx_high; i++){
-	//DREAL_LOG_INFO << i << " " << var((*trail)[i]);
+        //DREAL_LOG_INFO << i << " " << var((*trail)[i]);
         if (var((*trail)[i]) > 1) // 0 and 1 are false and true
           DREAL_LOG_INFO << i << ":\t"<<  theory_handler->varToEnode(var((*trail)[i])) << " = " << !sign((*trail)[i]);
       }
@@ -123,7 +123,7 @@ namespace dreal{
 
       DREAL_LOG_INFO << " -- LEVEL " << level << " (" << indx_low << ", " << indx_high << ") -- ";
       for (int i = indx_low; i < indx_high; i++){
-	DREAL_LOG_INFO << i << ":\t"<<  m_stack[i]->first << " = " << m_stack[i]->second;
+        DREAL_LOG_INFO << i << ":\t"<<  m_stack[i]->first << " = " << m_stack[i]->second;
       }
     }
    DREAL_LOG_INFO << " -- End Stack --";
@@ -135,10 +135,10 @@ namespace dreal{
     // return true if no suggestion is inconsistent with the stack
     for(auto sug : m_suggestions){
       for(auto sta : m_stack){
-	if(sug->first == sta->first && sug->second != sta->second) {
-	  DREAL_LOG_DEBUG << "Stack and Suggestion Inconsistent: " << sug->first << " = " << sug->second << " " << sta->first << " = "  <<  sta->second;
-	  return false;
-	}
+        if(sug->first == sta->first && sug->second != sta->second) {
+          DREAL_LOG_DEBUG << "Stack and Suggestion Inconsistent: " << sug->first << " = " << sug->second << " " << sta->first << " = "  <<  sta->second;
+          return false;
+        }
       }
     }
     return true;

diff --git a/src/opensmt/heuristics/heuristic.h b/src/opensmt/heuristics/heuristic.h
@@ -34,7 +34,7 @@ namespace dreal {
   heuristic() : m_is_initialized(false), backtracked(false), lastTrailEnd(2) {}
     virtual ~heuristic();
     virtual void initialize(SMTConfig &, Egraph &, THandler* thandler,
-		    vec<Lit> *trail, vec<int> *trail_lim);
+                    vec<Lit> *trail, vec<int> *trail_lim);
     virtual void inform(Enode * e);
     virtual void backtrack();
     virtual Lit getSuggestion();