Formatting, mostly tabs

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/ast/ast.cpp

@@ -2848,7 +2848,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
         SASSERT(is_or(f1));
         app * cls            = to_app(f1);
         unsigned cls_sz      = cls->get_num_args();
-		CTRACE("cunit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))),
+        CTRACE("cunit_bug", !(num_proofs == cls_sz || (num_proofs == cls_sz + 1 && is_false(new_fact))),
           for (unsigned i = 0; i < num_proofs; i++) tout << mk_pp(get_fact(proofs[i]), *this) << "\n";
           tout << "===>\n";
           tout << mk_pp(new_fact, *this) << "\n";);

src/ast/ast_smt_pp.cpp

@@ -1003,7 +1003,7 @@ public:
             visit_sort(d->get_domain(i), true);
         }
         m_out << ")";
-	}
+    }
 };
 
 

src/ast/bv_decl_plugin.cpp

@@ -136,7 +136,7 @@ void bv_decl_plugin::finalize() {
     for (; it != end; ++it) {
         ptr_vector<func_decl> & ds = *it;
         DEC_REF(ds);
-	}
+    }
     DEC_REF(m_mkbv);
 }
 
@@ -157,13 +157,13 @@ void bv_decl_plugin::mk_bv_sort(unsigned bv_size) {
 }
 
 inline sort * bv_decl_plugin::get_bv_sort(unsigned bv_size) {
-	if (bv_size < (1 << 12)) {
-	    mk_bv_sort(bv_size);
+    if (bv_size < (1 << 12)) {
+        mk_bv_sort(bv_size);
             return m_bv_sorts[bv_size];
-	}
-	parameter p(bv_size);
-	sort_size sz(sort_size::mk_very_big());
-	return m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p));
+    }
+    parameter p(bv_size);
+    sort_size sz(sort_size::mk_very_big());
+    return m_manager->mk_sort(symbol("bv"), sort_info(m_family_id, BV_SORT, sz, 1, &p));
 }
 
 sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {

src/ast/datatype_decl_plugin.cpp

@@ -919,9 +919,9 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
     todo.push_back(s0);
     mark.mark(s0, true);
     while (!todo.empty()) {
-		sort* s = todo.back();
+        sort* s = todo.back();
         todo.pop_back();
-		strm << s->get_name() << " =\n";
+        strm << s->get_name() << " =\n";
 
         ptr_vector<func_decl> const * cnstrs = get_datatype_constructors(s);
         for (unsigned i = 0; i < cnstrs->size(); ++i) {
@@ -931,14 +931,14 @@ void datatype_util::display_datatype(sort *s0, std::ostream& strm) {
             ptr_vector<func_decl> const * accs = get_constructor_accessors(cns);
             for (unsigned j = 0; j < accs->size(); ++j) {
                 func_decl* acc = (*accs)[j];
-				sort* s1 = acc->get_range();
+                sort* s1 = acc->get_range();
                 strm << "(" << acc->get_name() << ": " << s1->get_name() << ") "; 
                 if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) {
                         mark.mark(s1, true);
                         todo.push_back(s1);
                 }          
             }
-			strm << "\n";
+            strm << "\n";
         }
     }
 

src/ast/simplifier/distribute_forall.cpp

@@ -148,7 +148,7 @@ void distribute_forall::operator()(expr * f, expr_ref & result) {
 
     while (!m_todo.empty()) {
         expr * e = m_todo.back();
-        if (visit_children(e)) {	        
+        if (visit_children(e)) {            
             m_todo.pop_back();
             reduce1(e);
         }                

src/cmd_context/basic_cmds.cpp

@@ -255,7 +255,7 @@ protected:
             s == m_print_success || s == m_print_warning || s == m_expand_definitions || 
             s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores ||
             s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants ||
-	    s == m_regular_output_channel || s == m_diagnostic_output_channel || 
+        s == m_regular_output_channel || s == m_diagnostic_output_channel || 
             s == m_random_seed || s == m_verbosity || s == m_global_decls;
     }
 

src/muz/base/dl_boogie_proof.cpp

@@ -142,7 +142,7 @@ namespace datalog {
         steps.push_back(step());
         obj_map<proof, unsigned> index;
         index.insert(m_proof, 0);
-		
+        
         for (unsigned j = 0; j < rules.size(); ++j) {
             proof* p = rules[j];
             proof_ref_vector premises(m);

src/muz/base/dl_context.cpp

@@ -963,12 +963,12 @@ namespace datalog {
         // TODO: what?
         if(get_engine() != DUALITY_ENGINE) {
           new_query();
-	  rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
-	  rule_ref r(m_rule_manager);
-	  for (; it != end; ++it) {
+      rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
+      rule_ref r(m_rule_manager);
+      for (; it != end; ++it) {
             r = *it;
             check_rule(r);
-	  }     
+      }     
         }   
 #endif
         m_mc = mk_skip_model_converter();
@@ -985,10 +985,10 @@ namespace datalog {
             flush_add_rules();
             break;
         case DUALITY_ENGINE:
-	    // this lets us use duality with SAS 2013 abstraction
-	    if(quantify_arrays())
-	      flush_add_rules();
-	    break;
+            // this lets us use duality with SAS 2013 abstraction
+            if(quantify_arrays())
+              flush_add_rules();
+            break;
         default:
             UNREACHABLE();
         }
@@ -1109,11 +1109,11 @@ namespace datalog {
    
   void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, vector<unsigned> &bounds){
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
-	    expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
-	    rules.push_back(r.get());
-	    //            rules.push_back(m_rule_fmls[i].get());
-	    names.push_back(m_rule_names[i]);
-	    bounds.push_back(m_rule_bounds[i]);
+            expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
+            rules.push_back(r.get());
+            //            rules.push_back(m_rule_fmls[i].get());
+            names.push_back(m_rule_names[i]);
+            bounds.push_back(m_rule_bounds[i]);
         }
     }
 

src/muz/fp/dl_cmds.cpp

@@ -110,7 +110,7 @@ struct dl_context {
             m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
         }
         else {
-	    m_context->add_rule(rule, name, bound);
+        m_context->add_rule(rule, name, bound);
         }
     }    
 
@@ -260,11 +260,11 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
-	    if(dlctx.get_status() == datalog::BOUNDED){
-	      ctx.regular_stream() << "bounded\n";
-	      print_certificate(ctx);
-	      break;
-	    }
+            if(dlctx.get_status() == datalog::BOUNDED){
+              ctx.regular_stream() << "bounded\n";
+              print_certificate(ctx);
+              break;
+            }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {
             case datalog::INPUT_ERROR:

src/muz/transforms/dl_mk_bit_blast.cpp

@@ -219,7 +219,7 @@ namespace datalog {
 
     class mk_bit_blast::impl {
 
-        context &	     m_context;
+        context &         m_context;
         ast_manager &        m;
         params_ref           m_params;
         mk_interp_tail_simplifier m_simplifier;

src/tactic/aig/aig.cpp

@@ -1531,7 +1531,7 @@ public:
     catch (aig_exception ex) {
         dec_ref(r);
         throw ex;
-	}
+    }
         dec_ref_result(r);
         return r;
     }