From 1ebfcfc2cb37bc84ceedf73c3bf72df141520469 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 31 Oct 2012 14:21:22 -0700 Subject: [PATCH] removing fat Signed-off-by: Leonardo de Moura --- src/api/z3_logger.h | 53 ++++++++++--------- src/smt/smt_setup.cpp | 48 ++++++++--------- src/smt/theory_arith.cpp | 4 +- src/smt/theory_arith.h | 106 +++++-------------------------------- src/smt/theory_arith_aux.h | 94 ++++++++++++++++++++++++++++++++ 5 files changed, 161 insertions(+), 144 deletions(-) diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 8e2867795..4d83f90c2 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -19,6 +19,33 @@ Notes: #include #include"symbol.h" struct ll_escaped { char const * m_str; ll_escaped(char const * str):m_str(str) {} }; +static std::ostream & operator<<(std::ostream & out, ll_escaped const & d); + +static void __declspec(noinline) R() { *g_z3_log << "R\n"; g_z3_log->flush(); } +static void __declspec(noinline) P(void * obj) { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) I(__int64 i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) U(__uint64 u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } +static void __declspec(noinline) Sy(Z3_symbol sym) { + symbol s = symbol::mk_symbol_from_c_ptr(reinterpret_cast(sym)); + if (s == symbol::null) { + *g_z3_log << "N\n"; + } + else if (s.is_numerical()) { + *g_z3_log << "# " << s.get_num() << "\n"; + } + else { + *g_z3_log << "$ |" << ll_escaped(s.bare_str()) << "|\n"; + } + g_z3_log->flush(); +} +static void __declspec(noinline) Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); } +static void __declspec(noinline) C(unsigned id) { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); } +void __declspec(noinline) _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); } + static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { char const * s = d.m_str; while (*s) { @@ -42,29 +69,3 @@ static std::ostream & operator<<(std::ostream & out, ll_escaped const & d) { } return out; } - -static void R() { *g_z3_log << "R\n"; g_z3_log->flush(); } -static void P(void * obj) { *g_z3_log << "P " << obj << "\n"; g_z3_log->flush(); } -static void I(__int64 i) { *g_z3_log << "I " << i << "\n"; g_z3_log->flush(); } -static void U(__uint64 u) { *g_z3_log << "U " << u << "\n"; g_z3_log->flush(); } -static void D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } -static void S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } -static void Sy(Z3_symbol sym) { - symbol s = symbol::mk_symbol_from_c_ptr(reinterpret_cast(sym)); - if (s == symbol::null) { - *g_z3_log << "N\n"; - } - else if (s.is_numerical()) { - *g_z3_log << "# " << s.get_num() << "\n"; - } - else { - *g_z3_log << "$ |" << ll_escaped(s.bare_str()) << "|\n"; - } - g_z3_log->flush(); -} -static void Ap(unsigned sz) { *g_z3_log << "p " << sz << "\n"; g_z3_log->flush(); } -static void Au(unsigned sz) { *g_z3_log << "u " << sz << "\n"; g_z3_log->flush(); } -static void Asy(unsigned sz) { *g_z3_log << "s " << sz << "\n"; g_z3_log->flush(); } -static void C(unsigned id) { *g_z3_log << "C " << id << "\n"; g_z3_log->flush(); } -void _Z3_append_log(char const * msg) { *g_z3_log << "M \"" << ll_escaped(msg) << "\"\n"; g_z3_log->flush(); } - diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 72d596ab9..63fe1b7f3 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -282,14 +282,14 @@ namespace smt { } else { if (m_params.m_arith_auto_config_simplex || st.m_num_uninterpreted_constants > 4 * st.m_num_bool_constants) { - if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8)) { - TRACE("rdl_bug", tout << "using theory_smi_arith\n";); - m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params)); - } - else { - TRACE("rdl_bug", tout << "using theory_mi_arith\n";); - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - } + // if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8)) { + // TRACE("rdl_bug", tout << "using theory_smi_arith\n";); + // m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params)); + // } + // else { + TRACE("rdl_bug", tout << "using theory_mi_arith\n";); + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); + // } } else { m_params.m_arith_bound_prop = BP_NONE; @@ -362,14 +362,14 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params)); } else { - if (st.m_arith_k_sum < rational(INT_MAX / 8)) { - TRACE("setup", tout << "using small integer simplex...\n";); - m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); - } - else { - TRACE("setup", tout << "using big integer simplex...\n";); - m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); - } + // if (st.m_arith_k_sum < rational(INT_MAX / 8)) { + // TRACE("setup", tout << "using small integer simplex...\n";); + // m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); + // } + // else { + TRACE("setup", tout << "using big integer simplex...\n";); + m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); + // } } } @@ -421,8 +421,8 @@ namespace smt { if (m_params.m_proof_mode != PGM_DISABLED) { m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); } - else if (st.m_arith_k_sum < rational(INT_MAX / 8)) - m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); + // else if (st.m_arith_k_sum < rational(INT_MAX / 8)) + // m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); else m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); } @@ -758,12 +758,12 @@ namespace smt { if (m_params.m_proof_mode != PGM_DISABLED) { m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); } - else if (m_params.m_arith_fixnum) { - if (m_params.m_arith_int_only) - m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); - else - m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params)); - } + // else if (m_params.m_arith_fixnum) { + // if (m_params.m_arith_int_only) + // m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); + // else + // m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params)); + // } else { if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp index 6aa0e1370..d57812b7a 100644 --- a/src/smt/theory_arith.cpp +++ b/src/smt/theory_arith.cpp @@ -24,7 +24,7 @@ namespace smt { template class theory_arith; template class theory_arith; template class theory_arith; - template class theory_arith; - template class theory_arith; + // template class theory_arith; + // template class theory_arith; }; diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index bb09d68b7..c125558f7 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -145,12 +145,7 @@ namespace smt { unsigned m_size; // the real size, m_entries contains dead row_entries. int m_base_var; int m_first_free_idx; // first available position. - row(): - m_size(0), - m_base_var(null_theory_var), - m_first_free_idx(-1) { - } - + row(); unsigned size() const { return m_size; } unsigned num_entries() const { return m_entries.size(); } void reset(); @@ -231,65 +226,21 @@ namespace smt { return m_eq_coeffs.empty() && m_lit_coeffs.empty(); } - void init() { - if (!m_init && !empty()) { - m_params.push_back(parameter(symbol("unknown-arith"))); - for (unsigned i = 0; i < m_lits.size(); i++) { - m_params.push_back(parameter(m_lit_coeffs[i].to_rational())); - } - for (unsigned i = 0; i < m_eqs.size(); i++) { - m_params.push_back(parameter(m_eq_coeffs[i].to_rational())); - } - m_init = true; - } - } + void init(); + public: antecedents(): m_init(false) {} - - void reset() { - m_init = false; - m_eq_coeffs.reset(); - m_lit_coeffs.reset(); - m_eqs.reset(); - m_lits.reset(); - m_params.reset(); - } - + void reset(); literal_vector& lits() { return m_lits; } - eq_vector& eqs() { return m_eqs; } - - void push_lit(literal l, numeral const& r) { - m_lits.push_back(l); - if (proofs_enabled) { - m_lit_coeffs.push_back(r); - } - } - - void push_eq(enode_pair const& p, numeral const& r) { - m_eqs.push_back(p); - if (proofs_enabled) { - m_eq_coeffs.push_back(r); - } - } - - - unsigned num_params() const { - return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; - } - + void push_lit(literal l, numeral const& r); + void push_eq(enode_pair const& p, numeral const& r); + unsigned num_params() const { return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; } numeral const* lit_coeffs() const { return m_lit_coeffs.c_ptr(); } numeral const* eq_coeffs() const { return m_eq_coeffs.c_ptr(); } - - parameter* params(char const* name) { - if (empty()) return 0; - init(); - m_params[0] = parameter(symbol(name)); - return m_params.c_ptr(); - } + parameter* params(char const* name); }; - class bound { protected: theory_var m_var; @@ -567,15 +518,7 @@ namespace smt { bool above_upper(theory_var v) const { bound * u = upper(v); return u != 0 && get_value(v) > u->get_value(); } bool below_upper(theory_var v) const { bound * u = upper(v); return u == 0 || get_value(v) < u->get_value(); } bool above_lower(theory_var v) const { bound * l = lower(v); return l == 0 || get_value(v) > l->get_value(); } - - bool at_bound(theory_var v) const { - bound * l = lower(v); - if (l != 0 && get_value(v) == l->get_value()) - return true; - bound * u = upper(v); - return u != 0 && get_value(v) == u->get_value(); - } - + bool at_bound(theory_var v) const; bool at_lower(theory_var v) const { bound * l = lower(v); return l != 0 && get_value(v) == l->get_value(); } bool at_upper(theory_var v) const { bound * u = upper(v); return u != 0 && get_value(v) == u->get_value(); } bool is_free(theory_var v) const { return lower(v) == 0 && upper(v) == 0; } @@ -585,33 +528,12 @@ namespace smt { SASSERT(get_context().e_internalized(n) && get_context().get_enode(n)->get_th_var(get_id()) != null_theory_var); return is_free(get_context().get_enode(n)->get_th_var(get_id())); } - - bool is_fixed(theory_var v) const { - bound * l = lower(v); - if (l == 0) - return false; - bound * u = upper(v); - if (u == 0) - return false; - return l->get_value() == u->get_value(); - } - + bool is_fixed(theory_var v) const; void set_bound_core(theory_var v, bound * new_bound, bool upper) { m_bounds[static_cast(upper)][v] = new_bound; } void restore_bound(theory_var v, bound * new_bound, bool upper) { set_bound_core(v, new_bound, upper); } void restore_nl_propagated_flag(unsigned old_trail_size); - - void set_bound(bound * new_bound, bool upper) { - SASSERT(new_bound); - SASSERT(!upper || new_bound->get_bound_kind() == B_UPPER); - SASSERT(upper || new_bound->get_bound_kind() == B_LOWER); - theory_var v = new_bound->get_var(); - set_bound_core(v, new_bound, upper); - if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v)) - fixed_var_eh(v); - } - + void set_bound(bound * new_bound, bool upper); inf_numeral const & get_epsilon(theory_var v) const { return is_real(v) ? this->m_real_epsilon : this->m_int_epsilon; } - bool enable_cgc_for(app * n) const; enode * mk_enode(app * n); void mk_enode_if_reflect(app * n); @@ -1171,7 +1093,7 @@ namespace smt { static const bool proofs_enabled = false; i_ext() : m_int_epsilon(1), m_real_epsilon(1) {} }; - + class si_ext { public: typedef s_integer numeral; @@ -1213,8 +1135,8 @@ namespace smt { typedef theory_arith theory_mi_arith; typedef theory_arith theory_mi_arith_w_proofs; typedef theory_arith theory_i_arith; - typedef theory_arith theory_si_arith; - typedef theory_arith theory_smi_arith; + // typedef theory_arith theory_si_arith; + // typedef theory_arith theory_smi_arith; }; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index bff567f1b..4d22287ed 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -28,6 +28,13 @@ namespace smt { // Rows // // ----------------------------------- + + template + theory_arith::row::row(): + m_size(0), + m_base_var(null_theory_var), + m_first_free_idx(-1) { + } template void theory_arith::row::reset() { @@ -298,6 +305,60 @@ namespace smt { m_size--; } + // ----------------------------------- + // + // Antecedents + // + // ----------------------------------- + + template + void theory_arith::antecedents::init() { + if (!m_init && !empty()) { + m_params.push_back(parameter(symbol("unknown-arith"))); + for (unsigned i = 0; i < m_lits.size(); i++) { + m_params.push_back(parameter(m_lit_coeffs[i].to_rational())); + } + for (unsigned i = 0; i < m_eqs.size(); i++) { + m_params.push_back(parameter(m_eq_coeffs[i].to_rational())); + } + m_init = true; + } + } + + template + void theory_arith::antecedents::reset() { + m_init = false; + m_eq_coeffs.reset(); + m_lit_coeffs.reset(); + m_eqs.reset(); + m_lits.reset(); + m_params.reset(); + } + + template + void theory_arith::antecedents::push_lit(literal l, numeral const& r) { + m_lits.push_back(l); + if (proofs_enabled) { + m_lit_coeffs.push_back(r); + } + } + + template + void theory_arith::antecedents::push_eq(enode_pair const& p, numeral const& r) { + m_eqs.push_back(p); + if (proofs_enabled) { + m_eq_coeffs.push_back(r); + } + } + + template + parameter * theory_arith::antecedents::params(char const* name) { + if (empty()) return 0; + init(); + m_params[0] = parameter(symbol(name)); + return m_params.c_ptr(); + } + // ----------------------------------- // // Atoms @@ -342,6 +403,39 @@ namespace smt { // // ----------------------------------- + template + bool theory_arith::at_bound(theory_var v) const { + bound * l = lower(v); + if (l != 0 && get_value(v) == l->get_value()) + return true; + bound * u = upper(v); + return u != 0 && get_value(v) == u->get_value(); + } + + template + bool theory_arith::is_fixed(theory_var v) const { + bound * l = lower(v); + if (l == 0) + return false; + bound * u = upper(v); + if (u == 0) + return false; + return l->get_value() == u->get_value(); + } + + template + void theory_arith::set_bound(bound * new_bound, bool upper) { + SASSERT(new_bound); + SASSERT(!upper || new_bound->get_bound_kind() == B_UPPER); + SASSERT(upper || new_bound->get_bound_kind() == B_LOWER); + theory_var v = new_bound->get_var(); + set_bound_core(v, new_bound, upper); + if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v)) + fixed_var_eh(v); + } + + + /** \brief Return the col_entry that points to a base row that contains the given variable. Return 0 if no row contains v.