mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

removed template specialization overkill

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-05 08:56:19 -08:00
parent 5379130c8c
commit 3736c5ea3b
5 changed files with 38 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/smt/smt_setup.cpp
View file

@ -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;
}
}

1
src/smt/theory_arith.cpp
View file

@ -21,7 +21,6 @@ Revision History:
namespace smt {
template class theory_arith<mi_ext_with_proofs>;
template class theory_arith<mi_ext>;
template class theory_arith<i_ext>;
// template class theory_arith<si_ext>;

43
src/smt/theory_arith.h
View file

@ -87,8 +87,8 @@ namespace smt {
typedef vector<numeral> 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<mi_ext> theory_mi_arith;
typedef theory_arith<mi_ext_with_proofs> theory_mi_arith_w_proofs;
typedef theory_arith<i_ext> theory_i_arith;
// typedef theory_arith<si_ext> theory_si_arith;
// typedef theory_arith<smi_ext> theory_smi_arith;

22
src/smt/theory_arith_aux.h
View file

@ -336,7 +336,7 @@ namespace smt {
}
template<typename Ext>
void theory_arith<Ext>::antecedents::push_lit(literal l, numeral const& r) {
void theory_arith<Ext>::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<typename Ext>
void theory_arith<Ext>::antecedents::push_eq(enode_pair const& p, numeral const& r) {
void theory_arith<Ext>::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<typename Ext>
void theory_arith<Ext>::derived_bound::push_justification(antecedents& a, numeral const& coeff) {
void theory_arith<Ext>::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<typename Ext>
void theory_arith<Ext>::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff) {
void theory_arith<Ext>::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<typename Ext>
void theory_arith<Ext>::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();

8
src/smt/theory_arith_core.h
View file

@ -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";
}
}