mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

patch bounds normalization bug found by dvitek

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-19 17:59:20 -07:00
parent e3a854743b
commit 8a63ae0cdf
2 changed files with 34 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/weighted_maxsat.cpp
View file

@ -768,7 +768,7 @@ namespace opt {
m_upper += m_weights[i];
}
}
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << " )\n";);
IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";);
fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
s.assert_expr(fml);
was_sat = true;

35
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -109,6 +109,18 @@ struct bv_size_reduction_tactic::imp {
}
}
void ensure_signed(app* lhs, numeral& n) {
}
bool at_upper(app* lhs, numeral const& n) {
return false;
}
bool at_lower(app* lhs, numeral const& n) {
return false;
}
void collect_bounds(goal const & g) {
unsigned sz = g.size();
numeral val;
@ -123,16 +135,35 @@ struct bv_size_reduction_tactic::imp {
}
if (m_util.is_bv_sle(f, lhs, rhs)) {
bv_sz = m_util.get_bv_size(lhs);
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// v <= k
if (negated) update_signed_lower(to_app(lhs), val+numeral(1));
val = m_util.norm(val, bv_sz, true);
if (negated) {
val += numeral(1);
if (m_util.norm(val, bv_sz, true) != val) {
// bound is infeasible.
}
else {
update_signed_lower(to_app(lhs), val);
}
}
else update_signed_upper(to_app(lhs), val);
}
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// k <= v
if (negated) update_signed_upper(to_app(rhs), val-numeral(1));
val = m_util.norm(val, bv_sz, true);
if (negated) {
val -= numeral(1);
if (m_util.norm(val, bv_sz, true) != val) {
// bound is infeasible.
}
else {
update_signed_upper(to_app(lhs), val);
}
}
else update_signed_lower(to_app(rhs), val);
}
}