Merge branch 'master' of https://github.com/Z3Prover/z3

src/ast/datatype_decl_plugin.cpp

@@ -935,9 +935,9 @@ bool datatype_util::is_recursive(sort * ty) {
 
 
 bool datatype_util::is_enum_sort(sort* s) {
-	if (!is_datatype(s)) {
+    if (!is_datatype(s)) {
-		return false;
+        return false;
-	}
+    }
     bool r = false;
     if (m_is_enum.find(s, r))
         return r;

src/ast/fpa/fpa2bv_rewriter.cpp

@@ -143,11 +143,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
         case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
         case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
-		case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
+        case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
         case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
         case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;
 

src/ast/rewriter/seq_rewriter.cpp

@@ -92,25 +92,25 @@ public:
         expr_ref fml(m.mk_true(), m);
         return sym_expr::mk_pred(fml, m.mk_bool_sort());
     }
-	virtual T mk_and(T x, T y) {
+    virtual T mk_and(T x, T y) {
-		if (x->is_char() && y->is_char()) {
+        if (x->is_char() && y->is_char()) {
-			if (x->get_char() == y->get_char()) {
+            if (x->get_char() == y->get_char()) {
-				return x;
+                return x;
-			}
+            }
-			if (m.are_distinct(x->get_char(), y->get_char())) {
+            if (m.are_distinct(x->get_char(), y->get_char())) {
-				expr_ref fml(m.mk_false(), m);
+                expr_ref fml(m.mk_false(), m);
-				return sym_expr::mk_pred(fml, x->get_sort());
+                return sym_expr::mk_pred(fml, x->get_sort());
-			}
+            }
-		}
+        }
 
-		sort* s = x->get_sort();
+        sort* s = x->get_sort();
-		if (m.is_bool(s)) s = y->get_sort();
+        if (m.is_bool(s)) s = y->get_sort();
-		var_ref v(m.mk_var(0, s), m);
+        var_ref v(m.mk_var(0, s), m);
-		expr_ref fml1 = x->accept(v);
+        expr_ref fml1 = x->accept(v);
-		expr_ref fml2 = y->accept(v);
+        expr_ref fml2 = y->accept(v);
-		if (m.is_true(fml1)) {
+        if (m.is_true(fml1)) {
-			return y;
+            return y;
-		}
+        }
         if (m.is_true(fml2)) return x;
         expr_ref fml(m.mk_and(fml1, fml2), m);
         return sym_expr::mk_pred(fml, x->get_sort());
@@ -178,10 +178,10 @@ public:
         return sym_expr::mk_pred(fml, x->get_sort());
     }
 
-	/*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
+    /*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
-		
+        
-		return 0;
+        return 0;
-	}*/
+    }*/
 };
 
 re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}

src/ast/static_features.cpp

@@ -391,7 +391,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
     if (is_marked(e)) {
         m_num_sharing++;
         return;
-    }	
+    }    
     if (stack_depth > m_max_stack_depth) {
         return;
     }

src/muz/pdr/pdr_context.cpp

@@ -1728,7 +1728,7 @@ namespace pdr {
 
     void context::validate_search() {
         expr_ref tr = m_search.get_trace(*this);
-		TRACE("pdr", tout << tr << "\n";);
+        TRACE("pdr", tout << tr << "\n";);
         smt::kernel solver(m, get_fparams());
         solver.assert_expr(tr);
         lbool res = solver.check();

src/smt/smt_case_split_queue.cpp

@@ -51,9 +51,9 @@ namespace smt {
             if (!m_theory_var_priority.find(v2, p_v2)) {
                 p_v2 = 0.0;
             }
-	    // add clause activity
+        // add clause activity
-	    p_v1 += m_activity[v1];
+        p_v1 += m_activity[v1];
-	    p_v2 += m_activity[v2];
+        p_v2 += m_activity[v2];
             return p_v1 > p_v2;
         }
     };

src/smt/smt_context.cpp

@@ -3035,7 +3035,7 @@ namespace smt {
         // not counting any literals that get assigned by this method
         // this relies on bcp() to give us its old m_qhead and therefore
         // bcp() should always be called before this method
-	
+    
         unsigned assigned_literal_end = m_assigned_literals.size();
         for (; qhead < assigned_literal_end; ++qhead) {
             literal l = m_assigned_literals[qhead];

src/smt/smt_for_each_relevant_expr.cpp

@@ -23,7 +23,7 @@ Revision History:
 
 namespace smt {
 
-	bool check_at_labels::check(expr* n) {
+    bool check_at_labels::check(expr* n) {
         m_first = true;
         return count_at_labels_pos(n) <= 1;
     }

src/smt/smt_model_checker.cpp

@@ -279,7 +279,7 @@ namespace smt {
             m_aux_context->pop(1);
             return r == l_false; // quantifier is satisfied by m_curr_model
         }
-		
+        
         model_ref complete_cex;
         m_aux_context->get_model(complete_cex); 
         
@@ -425,7 +425,7 @@ namespace smt {
         ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
         for (; it != end; ++it) {
             quantifier * q = *it;
-	    if(!m_qm->mbqi_enabled(q)) continue;
+        if(!m_qm->mbqi_enabled(q)) continue;
             TRACE("model_checker", 
                   tout << "Check: " << mk_pp(q, m) << "\n";
                   tout << m_context->get_assignment(q) << "\n";);

src/smt/theory_array_base.cpp

@@ -426,19 +426,19 @@ namespace smt {
         ptr_buffer<enode> to_unmark;
         unsigned num_vars = get_num_vars();
         for (unsigned i = 0; i < num_vars; i++) {
-	    enode * n = get_enode(i);
+        enode * n = get_enode(i);
             if (ctx.is_relevant(n)) {
-	        enode * r = n->get_root();
+            enode * r = n->get_root();
-		if (!r->is_marked()){
+        if (!r->is_marked()){
-		    if(is_array_sort(r) && ctx.is_shared(r)) {
+            if(is_array_sort(r) && ctx.is_shared(r)) {
-		      TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
+              TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
-		      theory_var r_th_var = r->get_th_var(get_id());
+              theory_var r_th_var = r->get_th_var(get_id());
-		      SASSERT(r_th_var != null_theory_var);
+              SASSERT(r_th_var != null_theory_var);
-		      result.push_back(r_th_var);
+              result.push_back(r_th_var);
-		    }
+            }
-		    r->set_mark();
+            r->set_mark();
-		    to_unmark.push_back(r);
+            to_unmark.push_back(r);
-		}
+        }
             }
         }
         unmark_enodes(to_unmark.size(), to_unmark.c_ptr());

src/smt/theory_str.cpp

@@ -5565,7 +5565,7 @@ namespace smt {
                         if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
                             ndVec.pop_back();
                             ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
-                            for (int i = 1; i < arg1VecSize; i++) {
+                            for (size_t i = 1; i < arg1VecSize; i++) {
                                 ndVec.push_back(arg1_grdItor->first[i]);
                             }
                         } else {
@@ -5668,7 +5668,7 @@ namespace smt {
         if (subStrCnt == 1) {
             zstring subStrVal;
             if (u.str.is_string(subStrVec[0], subStrVal)) {
-                for (int i = 0; i < strCnt; i++) {
+                for (size_t i = 0; i < strCnt; i++) {
                     zstring strVal;
                     if (u.str.is_string(strVec[i], strVal)) {
                         if (strVal.contains(subStrVal)) {
@@ -5677,7 +5677,7 @@ namespace smt {
                     }
                 }
             } else {
-                for (int i = 0; i < strCnt; i++) {
+                for (size_t i = 0; i < strCnt; i++) {
                     if (strVec[i] == subStrVec[0]) {
                         return true;
                     }
@@ -5685,7 +5685,7 @@ namespace smt {
             }
             return false;
         } else {
-            for (int i = 0; i <= (strCnt - subStrCnt); i++) {
+            for (size_t i = 0; i <= (strCnt - subStrCnt); i++) {
                 // The first node in subStrVect should be
                 //   * constant: a suffix of a note in strVec[i]
                 //   * variable:
@@ -5714,7 +5714,7 @@ namespace smt {
 
                 // middle nodes
                 bool midNodesOK = true;
-                for (int j = 1; j < subStrCnt - 1; j++) {
+                for (size_t j = 1; j < subStrCnt - 1; j++) {
                     if (subStrVec[j] != strVec[i + j]) {
                         midNodesOK = false;
                         break;

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -103,7 +103,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
     tactic * st = main_p(and_then(preamble_st,
                                   // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
                                   // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively,
-								  // the UFs can be eliminated by eager ackermannization in the preamble.
+                                  // the UFs can be eliminated by eager ackermannization in the preamble.
                                   cond(mk_is_qfbv_eq_probe(),
                                        and_then(mk_bv1_blaster_tactic(m),
                                                 using_params(smt, solver_p)),

src/util/hwf.cpp

@@ -29,7 +29,7 @@ Revision History:
 #include<fenv.h>
 #endif
 
-#if defined(__x86_64__) || defined(_M_X64) ||	\
+#if defined(__x86_64__) || defined(_M_X64) ||    \
     defined(__i386) || defined(_M_IX86)
 #define USE_INTRINSICS
 #endif

src/util/trace.cpp

@@ -52,7 +52,7 @@ void disable_trace(const char * tag) {
 
 bool is_trace_enabled(const char * tag) {
     return g_enable_all_trace_tags || 
-		(g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
+        (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
 }
 
 void close_trace() {

src/util/warning.cpp

@@ -115,22 +115,22 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
     while (true) {
         int nc = VPRF(buff.c_ptr(), buff.size(), msg, args);                                                
 #if !defined(_WINDOWS) && defined(_AMD64_)
-	// For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
+    // For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
-	// Z3 crashes when trying to use va_list args again.
+    // Z3 crashes when trying to use va_list args again.
         // Hack: I truncate the message instead of expanding the buffer to make sure that
         // va_list args is only used once.
-	END_ERR_HANDLER();
+    END_ERR_HANDLER();
-	if (nc < 0) {
+    if (nc < 0) {
-	  // vsnprintf didn't work, so we just print the msg
+      // vsnprintf didn't work, so we just print the msg
-	  out << msg; 
+      out << msg; 
-	  return;
+      return;
-	}
+    }
-	if (nc >= static_cast<int>(buff.size())) {
+    if (nc >= static_cast<int>(buff.size())) {
           // truncate the message
           buff[buff.size() - 1] = 0;
-	}
+    }
         out << buff.c_ptr();
-	return;
+    return;
 #else
         if (nc >= 0 && nc < static_cast<int>(buff.size()))
             break; // success