From 2a65503235805521134a53dbb7c6c45e75973fbe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Feb 2016 22:35:02 +0000 Subject: [PATCH] fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 2 +- src/opt/opt_context.cpp | 7 +++++-- src/smt/theory_bv.cpp | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 53f058fb4..813c0cd1c 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -173,7 +173,7 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp SASSERT(sz == out_bits.size()); return; } - + if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) { SASSERT(sz == out_bits.size()); return; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 97b8c999d..3c305723b 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -883,11 +883,11 @@ namespace opt { bool neg; if (is_maxsat(fml, terms, weights, offset, neg, id, index)) { objective& obj = m_objectives[index]; + if (obj.m_type != O_MAXSMT) { // change from maximize/minimize. obj.m_id = id; obj.m_type = O_MAXSMT; - obj.m_weights.append(weights); SASSERT(!m_maxsmts.contains(id)); add_maxsmt(id); } @@ -895,10 +895,13 @@ namespace opt { SASSERT(obj.m_id == id); obj.m_terms.reset(); obj.m_terms.append(terms); + obj.m_weights.reset(); + obj.m_weights.append(weights); obj.m_adjust_value.set_offset(offset); obj.m_adjust_value.set_negate(neg); m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value); - TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n";); + TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n"; + tout << terms << "\n";); } else if (is_maximize(fml, tr, orig_term, index)) { purify(tr); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e4f698914..94566c52b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -471,12 +471,12 @@ namespace smt { if (get_enode(v)->get_root() != get_enode(v2)->get_root()) { SASSERT(get_bv_size(v) == get_bv_size(v2)); context & ctx = get_context(); - justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2)); TRACE("fixed_var_eh", tout << "detected equality: v" << v << " = v" << v2 << "\n"; display_var(tout, v); display_var(tout, v2);); m_stats.m_num_th2core_eq++; add_fixed_eq(v, v2); + justification * js = ctx.mk_justification(fixed_eq_justification(*this, v, v2)); ctx.assign_eq(get_enode(v), get_enode(v2), eq_justification(js)); m_fixed_var_table.insert(key, v2); }