From a7d5bb7b36373e3e2e6b9a699687e1117b168e87 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 31 May 2017 12:18:00 +0100 Subject: [PATCH] Tabs --- src/ast/datatype_decl_plugin.cpp | 6 ++-- src/ast/fpa/fpa2bv_rewriter.cpp | 6 ++-- src/ast/rewriter/seq_rewriter.cpp | 44 +++++++++++++------------- src/ast/static_features.cpp | 2 +- src/muz/pdr/pdr_context.cpp | 2 +- src/smt/smt_case_split_queue.cpp | 6 ++-- src/smt/smt_context.cpp | 2 +- src/smt/smt_for_each_relevant_expr.cpp | 2 +- src/smt/smt_model_checker.cpp | 4 +-- src/smt/theory_array_base.cpp | 24 +++++++------- src/tactic/smtlogics/qfbv_tactic.cpp | 2 +- src/util/hwf.cpp | 2 +- src/util/trace.cpp | 2 +- src/util/warning.cpp | 22 ++++++------- 14 files changed, 63 insertions(+), 63 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 8ad33d6fc..4d531d2db 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/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)) { - return false; - } + if (!is_datatype(s)) { + return false; + } bool r = false; if (m_is_enum.find(s, r)) return r; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 725c0b043..32b62342b 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/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; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index dc1931bac..ce707b108 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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) { - if (x->is_char() && y->is_char()) { - if (x->get_char() == y->get_char()) { - return x; - } - if (m.are_distinct(x->get_char(), y->get_char())) { - expr_ref fml(m.mk_false(), m); - return sym_expr::mk_pred(fml, x->get_sort()); - } - } + virtual T mk_and(T x, T y) { + if (x->is_char() && y->is_char()) { + if (x->get_char() == y->get_char()) { + return x; + } + if (m.are_distinct(x->get_char(), y->get_char())) { + expr_ref fml(m.mk_false(), m); + return sym_expr::mk_pred(fml, x->get_sort()); + } + } - sort* s = x->get_sort(); - if (m.is_bool(s)) s = y->get_sort(); - var_ref v(m.mk_var(0, s), m); - expr_ref fml1 = x->accept(v); - expr_ref fml2 = y->accept(v); - if (m.is_true(fml1)) { - return y; - } + sort* s = x->get_sort(); + if (m.is_bool(s)) s = y->get_sort(); + var_ref v(m.mk_var(0, s), m); + expr_ref fml1 = x->accept(v); + expr_ref fml2 = y->accept(v); + if (m.is_true(fml1)) { + 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, T>> generate_min_terms(vector constraints){ - - return 0; - }*/ + /*virtual vector, T>> generate_min_terms(vector constraints){ + + return 0; + }*/ }; re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {} diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index daf20e095..a3ad7fd07 100644 --- a/src/ast/static_features.cpp +++ b/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; } diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 7484a77fa..05bb5489a 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/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(); diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 129d77c85..41a269820 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/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 - p_v1 += m_activity[v1]; - p_v2 += m_activity[v2]; + // add clause activity + p_v1 += m_activity[v1]; + p_v2 += m_activity[v2]; return p_v1 > p_v2; } }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 50b957331..0c32f3c76 100644 --- a/src/smt/smt_context.cpp +++ b/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]; diff --git a/src/smt/smt_for_each_relevant_expr.cpp b/src/smt/smt_for_each_relevant_expr.cpp index bf039e8a1..84f93dd33 100644 --- a/src/smt/smt_for_each_relevant_expr.cpp +++ b/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; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 279ea20cf..b50527acf 100644 --- a/src/smt/smt_model_checker.cpp +++ b/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::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";); diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index fa48fea57..6c47bf855 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -426,19 +426,19 @@ namespace smt { ptr_buffer 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(); - if (!r->is_marked()){ - if(is_array_sort(r) && ctx.is_shared(r)) { - TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); - theory_var r_th_var = r->get_th_var(get_id()); - SASSERT(r_th_var != null_theory_var); - result.push_back(r_th_var); - } - r->set_mark(); - to_unmark.push_back(r); - } + enode * r = n->get_root(); + if (!r->is_marked()){ + if(is_array_sort(r) && ctx.is_shared(r)) { + TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";); + theory_var r_th_var = r->get_th_var(get_id()); + SASSERT(r_th_var != null_theory_var); + result.push_back(r_th_var); + } + r->set_mark(); + to_unmark.push_back(r); + } } } unmark_enodes(to_unmark.size(), to_unmark.c_ptr()); diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 918e0fc6d..ca6390c9c 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/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)), diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index e577e15df..a522c9a41 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -29,7 +29,7 @@ Revision History: #include #endif -#if defined(__x86_64__) || defined(_M_X64) || \ +#if defined(__x86_64__) || defined(_M_X64) || \ defined(__i386) || defined(_M_IX86) #define USE_INTRINSICS #endif diff --git a/src/util/trace.cpp b/src/util/trace.cpp index 72984d808..05a3e49bd 100644 --- a/src/util/trace.cpp +++ b/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(tag))); + (g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast(tag))); } void close_trace() { diff --git a/src/util/warning.cpp b/src/util/warning.cpp index ed4cd8725..9c6a285b9 100644 --- a/src/util/warning.cpp +++ b/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. - // Z3 crashes when trying to use va_list args again. + // 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. // Hack: I truncate the message instead of expanding the buffer to make sure that // va_list args is only used once. - END_ERR_HANDLER(); - if (nc < 0) { - // vsnprintf didn't work, so we just print the msg - out << msg; - return; - } - if (nc >= static_cast(buff.size())) { + END_ERR_HANDLER(); + if (nc < 0) { + // vsnprintf didn't work, so we just print the msg + out << msg; + return; + } + if (nc >= static_cast(buff.size())) { // truncate the message buff[buff.size() - 1] = 0; - } + } out << buff.c_ptr(); - return; + return; #else if (nc >= 0 && nc < static_cast(buff.size())) break; // success