From 3736c5ea3b97521dad85cdc6262151fae2875ec5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Dec 2012 08:56:19 -0800 Subject: [PATCH] removed template specialization overkill Signed-off-by: Leonardo de Moura --- src/smt/smt_setup.cpp | 49 +++++++++++-------------------------- src/smt/theory_arith.cpp | 1 - src/smt/theory_arith.h | 43 +++++++------------------------- src/smt/theory_arith_aux.h | 22 ++++++++--------- src/smt/theory_arith_core.h | 8 +++--- 5 files changed, 38 insertions(+), 85 deletions(-) diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 77c1be886..ac31eb1a9 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -266,8 +266,8 @@ namespace smt { // Moreover, if model construction is enabled, then rational numbers may be needed // to compute the actual value of epsilon even if the input does not have rational numbers. // Example: (x < 1) and (x > 0) - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); + if (m_manager.proofs_enabled()) { + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); } else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8)) @@ -343,8 +343,8 @@ namespace smt { tout << "RELEVANCY: " << m_params.m_relevancy_lvl << "\n"; tout << "ARITH_EQ_BOUNDS: " << m_params.m_arith_eq_bounds << "\n";); - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); + if (m_manager.proofs_enabled()) { + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); } else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { TRACE("setup", tout << "using dense diff logic...\n";); @@ -394,8 +394,8 @@ namespace smt { m_params.m_lemma_gc_half = true; m_params.m_restart_strategy = RS_GEOMETRIC; - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); + if (m_manager.proofs_enabled()) { + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); } else if (st.m_arith_k_sum < rational(INT_MAX / 8)) m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params)); @@ -409,8 +409,8 @@ namespace smt { m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_factor = 1.5; m_params.m_restart_adaptive = false; - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); + if (m_manager.proofs_enabled()) { + m_context.register_plugin(alloc(smt::theory_mi_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)); @@ -683,21 +683,11 @@ namespace smt { } void setup::setup_i_arith() { - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); - } - else { - m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); - } + m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); } void setup::setup_mi_arith() { - if (m_manager.proof_mode() != PGM_DISABLED) { - m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); - } - else { - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - } + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); } void setup::setup_arith() { @@ -734,21 +724,10 @@ namespace smt { } break; default: - if (m_manager.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_int_only) - m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); - else - m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); - } + if (m_params.m_arith_int_only) + m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); + else + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); break; } } diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp index d57812b7a..0bb356b95 100644 --- a/src/smt/theory_arith.cpp +++ b/src/smt/theory_arith.cpp @@ -21,7 +21,6 @@ Revision History: namespace smt { - 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 c125558f7..9435a49cd 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -87,8 +87,8 @@ namespace smt { typedef vector numeral_vector; static const int dead_row_id = -1; - static const bool proofs_enabled = Ext::proofs_enabled; protected: + bool proofs_enabled() const { return get_manager().proofs_enabled(); } struct linear_monomial { numeral m_coeff; @@ -233,8 +233,8 @@ namespace smt { void reset(); literal_vector& lits() { return m_lits; } eq_vector& eqs() { return m_eqs; } - void push_lit(literal l, numeral const& r); - void push_eq(enode_pair const& p, numeral const& r); + void push_lit(literal l, numeral const& r, bool proofs_enabled); + void push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled); 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(); } @@ -284,8 +284,8 @@ namespace smt { bool is_true() const { return m_is_true; } void assign_eh(bool is_true, inf_numeral const & epsilon); virtual bool has_justification() const { return true; } - virtual void push_justification(antecedents& a, numeral const& coeff) { - a.push_lit(literal(get_bool_var(), !m_is_true), coeff); + virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { + a.push_lit(literal(get_bool_var(), !m_is_true), coeff, proofs_enabled); } }; @@ -301,9 +301,9 @@ namespace smt { } virtual ~eq_bound() {} virtual bool has_justification() const { return true; } - virtual void push_justification(antecedents& a, numeral const& coeff) { + virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { SASSERT(m_lhs->get_root() == m_rhs->get_root()); - a.push_eq(enode_pair(m_lhs, m_rhs), coeff); + a.push_eq(enode_pair(m_lhs, m_rhs), coeff, proofs_enabled); } }; @@ -316,7 +316,7 @@ namespace smt { derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {} virtual ~derived_bound() {} virtual bool has_justification() const { return true; } - virtual void push_justification(antecedents& a, numeral const& coeff); + virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled); virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); } virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); } }; @@ -329,7 +329,7 @@ namespace smt { justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {} virtual ~justified_derived_bound() {} virtual bool has_justification() const { return true; } - virtual void push_justification(antecedents& a, numeral const& coeff); + virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled); virtual void push_lit(literal l, numeral const& coeff); virtual void push_eq(enode_pair const& p, numeral const& coeff); @@ -1053,30 +1053,9 @@ namespace smt { static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) { return inf_numeral(n, r); } - static const bool proofs_enabled = false; mi_ext() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {} }; - class mi_ext_with_proofs { - public: - typedef rational numeral; - typedef inf_rational inf_numeral; - inf_numeral m_int_epsilon; - inf_numeral m_real_epsilon; - numeral fractional_part(inf_numeral const& n) { - SASSERT(n.is_rational()); - return n.get_rational() - floor(n); - } - static numeral fractional_part(numeral const & n) { - return n - floor(n); - } - static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) { - return inf_numeral(n, r); - } - static const bool proofs_enabled = true; - mi_ext_with_proofs() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {} - }; - class i_ext { public: typedef rational numeral; @@ -1090,7 +1069,6 @@ namespace smt { UNREACHABLE(); return inf_numeral(n); } - static const bool proofs_enabled = false; i_ext() : m_int_epsilon(1), m_real_epsilon(1) {} }; @@ -1107,7 +1085,6 @@ namespace smt { UNREACHABLE(); return inf_numeral(n); } - static const bool proofs_enabled = false; si_ext(): m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(1)) {} }; @@ -1128,12 +1105,10 @@ namespace smt { static inf_numeral mk_inf_numeral(numeral const& n, numeral const& i) { return inf_numeral(n, i); } - static const bool proofs_enabled = false; smi_ext() : m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(0), true) {} }; 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; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 4d22287ed..1e15365a4 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -336,7 +336,7 @@ namespace smt { } template - void theory_arith::antecedents::push_lit(literal l, numeral const& r) { + void theory_arith::antecedents::push_lit(literal l, numeral const& r, bool proofs_enabled) { m_lits.push_back(l); if (proofs_enabled) { m_lit_coeffs.push_back(r); @@ -344,7 +344,7 @@ namespace smt { } template - void theory_arith::antecedents::push_eq(enode_pair const& p, numeral const& r) { + void theory_arith::antecedents::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) { m_eqs.push_back(p); if (proofs_enabled) { m_eq_coeffs.push_back(r); @@ -690,14 +690,14 @@ namespace smt { // ----------------------------------- template - void theory_arith::derived_bound::push_justification(antecedents& a, numeral const& coeff) { + void theory_arith::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { if (proofs_enabled) { for (unsigned i = 0; i < m_lits.size(); ++i) { - a.push_lit(m_lits[i], coeff); + a.push_lit(m_lits[i], coeff, proofs_enabled); } for (unsigned i = 0; i < m_eqs.size(); ++i) { - a.push_eq(m_eqs[i], coeff); + a.push_eq(m_eqs[i], coeff, proofs_enabled); } } else { @@ -708,12 +708,12 @@ namespace smt { template - void theory_arith::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff) { + void theory_arith::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { for (unsigned i = 0; i < this->m_lits.size(); ++i) { - a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i]); + a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i], proofs_enabled); } for (unsigned i = 0; i < this->m_eqs.size(); ++i) { - a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i]); + a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i], proofs_enabled); } } @@ -755,7 +755,7 @@ namespace smt { literal l = ante.lits()[i]; if (lits.contains(l.index())) continue; - if (proofs_enabled) { + if (proofs_enabled()) { new_bound.push_lit(l, ante.lit_coeffs()[i]); } else { @@ -768,7 +768,7 @@ namespace smt { enode_pair const & p = ante.eqs()[i]; if (eqs.contains(p)) continue; - if (proofs_enabled) { + if (proofs_enabled()) { new_bound.push_eq(p, ante.eq_coeffs()[i]); } else { @@ -796,7 +796,7 @@ namespace smt { template void theory_arith::mk_bound_from_row(theory_var v, inf_numeral const & k, bound_kind kind, row const & r) { inf_numeral k_norm = normalize_bound(v, k, kind); - derived_bound * new_bound = proofs_enabled?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind); + derived_bound * new_bound = proofs_enabled()?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind); m_bounds_to_delete.push_back(new_bound); m_asserted_bounds.push_back(new_bound); m_tmp_lit_set.reset(); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a691096ec..0f3ed1d13 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2456,7 +2456,7 @@ namespace smt { delta -= coeff*(k_2 - k_1); } TRACE("propagate_bounds", tout << "delta (after replace): " << delta << "\n";); - new_atom->push_justification(ante, coeff); + new_atom->push_justification(ante, coeff, proofs_enabled()); SASSERT(delta >= inf_numeral::zero()); } } @@ -2569,7 +2569,7 @@ namespace smt { for (; it != end; ++it) lits.push_back(~(*it)); justification * js = 0; - if (proofs_enabled) { + if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr(), ante.num_params(), ante.params("assign-bounds")); } @@ -2656,13 +2656,13 @@ namespace smt { for (unsigned i = 0; i < num_literals; i++) { ctx.display_detailed_literal(tout, lits[i]); tout << " "; - if (proofs_enabled) { + if (proofs_enabled()) { tout << "bound: " << bounds.lit_coeffs()[i] << "\n"; } } for (unsigned i = 0; i < num_eqs; i++) { tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " "; - if (proofs_enabled) { + if (proofs_enabled()) { tout << "bound: " << bounds.eq_coeffs()[i] << "\n"; } }