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

fixing bug introduced today

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-05 16:21:53 -08:00
parent 2b66b50c75
commit 1a11196211
5 changed files with 21 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_arith.h
View file

@ -260,7 +260,7 @@ namespace smt {
bool is_atom() const { return m_atom; } bool is_atom() const { return m_atom; }
inf_numeral const & get_value() const { return m_value; } inf_numeral const & get_value() const { return m_value; }
virtual bool has_justification() const { return false; } virtual bool has_justification() const { return false; }
virtual void push_justification(antecedents& antecedents, numeral const& coeff) {} virtual void push_justification(antecedents& antecedents, numeral const& coeff, bool proofs_enabled) {}
}; };

2
src/smt/theory_arith_aux.h
View file

@ -749,7 +749,7 @@ namespace smt {
void theory_arith<Ext>::accumulate_justification(bound & b, derived_bound& new_bound, numeral const& coeff, literal_idx_set & lits, eq_set & eqs) { void theory_arith<Ext>::accumulate_justification(bound & b, derived_bound& new_bound, numeral const& coeff, literal_idx_set & lits, eq_set & eqs) {
antecedents& ante = m_tmp_antecedents; antecedents& ante = m_tmp_antecedents;
ante.reset(); ante.reset();
b.push_justification(ante, coeff); b.push_justification(ante, coeff, proofs_enabled());
unsigned num_lits = ante.lits().size(); unsigned num_lits = ante.lits().size();
for (unsigned i = 0; i < num_lits; ++i) { for (unsigned i = 0; i < num_lits; ++i) {
literal l = ante.lits()[i]; literal l = ante.lits()[i];

14
src/smt/theory_arith_core.h
View file

@ -1979,7 +1979,7 @@ namespace smt {
tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";); tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n";);
antecedents& ante = get_antecedents(); antecedents& ante = get_antecedents();
explain_bound(r, idx, !is_below, delta, ante); explain_bound(r, idx, !is_below, delta, ante);
b->push_justification(ante, numeral(1)); b->push_justification(ante, numeral(1), proofs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(), set_conflict(ante.lits().size(), ante.lits().c_ptr(),
@ -2122,8 +2122,8 @@ namespace smt {
void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) { void theory_arith<Ext>::sign_bound_conflict(bound * b1, bound * b2) {
SASSERT(b1->get_var() == b2->get_var()); SASSERT(b1->get_var() == b2->get_var());
antecedents& ante = get_antecedents(); antecedents& ante = get_antecedents();
b1->push_justification(ante, numeral(1)); b1->push_justification(ante, numeral(1), proofs_enabled());
b2->push_justification(ante, numeral(1)); b2->push_justification(ante, numeral(1), proofs_enabled());
set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas"); set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), ante, is_int(b1->get_var()), "farkas");
TRACE("arith_conflict", tout << "bound conflict\n";); TRACE("arith_conflict", tout << "bound conflict\n";);
@ -2382,7 +2382,7 @@ namespace smt {
if (!b->has_justification()) if (!b->has_justification())
continue; continue;
if (!relax_bounds() || delta.is_zero()) { if (!relax_bounds() || delta.is_zero()) {
b->push_justification(ante, it->m_coeff); b->push_justification(ante, it->m_coeff, proofs_enabled());
continue; continue;
} }
numeral coeff = it->m_coeff; numeral coeff = it->m_coeff;
@ -2442,7 +2442,7 @@ namespace smt {
SASSERT(!is_b_lower || k_2 <= k_1); SASSERT(!is_b_lower || k_2 <= k_1);
SASSERT(is_b_lower || k_2 >= k_1); SASSERT(is_b_lower || k_2 >= k_1);
if (new_atom == 0) { if (new_atom == 0) {
b->push_justification(ante, coeff); b->push_justification(ante, coeff, proofs_enabled());
continue; continue;
} }
SASSERT(!is_b_lower || k_2 < k_1); SASSERT(!is_b_lower || k_2 < k_1);
@ -2686,8 +2686,8 @@ namespace smt {
typename vector<row_entry>::const_iterator end = r.end_entries(); typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) { for (; it != end; ++it) {
if (!it->is_dead() && is_fixed(it->m_var)) { if (!it->is_dead() && is_fixed(it->m_var)) {
lower(it->m_var)->push_justification(antecedents, it->m_coeff); lower(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());
upper(it->m_var)->push_justification(antecedents, it->m_coeff); upper(it->m_var)->push_justification(antecedents, it->m_coeff, proofs_enabled());
} }
} }
} }

12
src/smt/theory_arith_eq.h
View file

@ -59,10 +59,10 @@ namespace smt {
// v >= k >= v2 => v >= v2 // v >= k >= v2 => v >= v2
// //
lower(v)->push_justification(ante, numeral::zero()); lower(v)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(v2)->push_justification(ante, numeral::zero()); upper(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
lower(v2)->push_justification(ante, numeral::zero()); lower(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(v)->push_justification(ante, numeral::zero()); upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n"; TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
display_var(tout, v); display_var(tout, v);
@ -247,8 +247,8 @@ namespace smt {
// //
// x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2 // x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2
// //
lower(x2)->push_justification(ante, numeral::zero()); lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(x2)->push_justification(ante, numeral::zero()); upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
m_stats.m_fixed_eqs++; m_stats.m_fixed_eqs++;
propagate_eq_to_core(x, x2, ante); propagate_eq_to_core(x, x2, ante);
} }

12
src/smt/theory_arith_int.h
View file

@ -525,7 +525,7 @@ namespace smt {
} }
// k += new_a_ij * lower_bound(x_j).get_rational(); // k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational()); k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero()); lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
} }
else { else {
SASSERT(at_upper(x_j)); SASSERT(at_upper(x_j));
@ -541,7 +541,7 @@ namespace smt {
} }
// k += new_a_ij * upper_bound(x_j).get_rational(); // k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational()); k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero()); upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
} }
pol.push_back(row_entry(new_a_ij, x_j)); pol.push_back(row_entry(new_a_ij, x_j));
} }
@ -566,7 +566,7 @@ namespace smt {
} }
// k += new_a_ij * lower_bound(x_j).get_rational(); // k += new_a_ij * lower_bound(x_j).get_rational();
k.addmul(new_a_ij, lower_bound(x_j).get_rational()); k.addmul(new_a_ij, lower_bound(x_j).get_rational());
lower(x_j)->push_justification(ante, numeral::zero()); lower(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
} }
else { else {
SASSERT(at_upper(x_j)); SASSERT(at_upper(x_j));
@ -579,7 +579,7 @@ namespace smt {
new_a_ij.neg(); // the upper terms are inverted new_a_ij.neg(); // the upper terms are inverted
// k += new_a_ij * upper_bound(x_j).get_rational(); // k += new_a_ij * upper_bound(x_j).get_rational();
k.addmul(new_a_ij, upper_bound(x_j).get_rational()); k.addmul(new_a_ij, upper_bound(x_j).get_rational());
upper(x_j)->push_justification(ante, numeral::zero()); upper(x_j)->push_justification(ante, numeral::zero(), proofs_enabled());
} }
TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";); TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << "\n";);
pol.push_back(row_entry(new_a_ij, x_j)); pol.push_back(row_entry(new_a_ij, x_j));
@ -772,8 +772,8 @@ namespace smt {
// u += ncoeff * lower_bound(v).get_rational(); // u += ncoeff * lower_bound(v).get_rational();
u.addmul(ncoeff, lower_bound(v).get_rational()); u.addmul(ncoeff, lower_bound(v).get_rational());
} }
lower(v)->push_justification(ante, numeral::zero()); lower(v)->push_justification(ante, numeral::zero(), proofs_enabled());
upper(v)->push_justification(ante, numeral::zero()); upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
} }
else if (gcds.is_zero()) { else if (gcds.is_zero()) {
gcds = abs_ncoeff; gcds = abs_ncoeff;