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

fix bug in simplifier of bv2int over concatentations exposed by

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-22 10:55:55 -07:00
parent e342b87921
commit 25d839ed10
3 changed files with 25 additions and 12 deletions

25
src/ast/simplifier/bv_simplifier_plugin.cpp
View file

@ -1517,13 +1517,24 @@ void bv_simplifier_plugin::mk_bv2int(expr * arg, sort* range, expr_ref & result)
result = m_arith.mk_add(tmp1, tmp2);
}
// commented out to reproduce bug in reduction of int2bv/bv2int
else if (m_util.is_concat(arg)) {
expr_ref tmp1(m_manager), tmp2(m_manager);
unsigned sz2 = get_bv_size(to_app(arg)->get_arg(1));
mk_bv2int(to_app(arg)->get_arg(0), range, tmp1);
mk_bv2int(to_app(arg)->get_arg(1), range, tmp2);
tmp1 = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz2), true), tmp1);
result = m_arith.mk_add(tmp1, tmp2);
else if (m_util.is_concat(arg) && to_app(arg)->get_num_args() > 0) {
expr_ref_vector args(m_manager);
unsigned num_args = to_app(arg)->get_num_args();
for (unsigned i = 0; i < num_args; ++i) {
expr_ref tmp(m_manager);
mk_bv2int(to_app(arg)->get_arg(i), range, tmp);
args.push_back(tmp);
}
unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
for (unsigned i = num_args - 1; i > 0; ) {
expr_ref tmp(m_manager);
--i;
tmp = args[i].get();
tmp = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz), true), tmp);
args[i] = tmp;
sz += get_bv_size(to_app(arg)->get_arg(i));
}
result = m_arith.mk_add(args.size(), args.c_ptr());
}
else {
parameter parameter(range);

7
src/smt/theory_arith_core.h
View file

@ -40,7 +40,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) {
if (!m_found_underspecified_op) {
TRACE("arith", tout << "found non underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
m_found_underspecified_op = true;
}
@ -395,6 +395,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_div(app * n) {
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
@ -418,7 +419,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_mod(app * n) {
TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
found_underspecified_op(n);
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy())
@ -428,7 +429,7 @@ namespace smt {
template<typename Ext>
theory_var theory_arith<Ext>::internalize_rem(app * n) {
found_underspecified_op(n);
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
theory_var s = mk_binary_op(n);
context & ctx = get_context();
if (!ctx.relevancy()) {

5
src/smt/theory_bv.cpp
View file

@ -607,12 +607,13 @@ namespace smt {
}
expr_ref sum(m);
arith_simp().mk_add(sz, args.c_ptr(), sum);
literal l(mk_eq(n, sum, false));
TRACE("bv",
tout << mk_pp(n, m) << "\n";
tout << mk_pp(sum, m) << "\n";
ctx.display_literal_verbose(tout, l);
tout << "\n";
);
literal l(mk_eq(n, sum, false));
ctx.mark_as_relevant(l);
ctx.mk_th_axiom(get_id(), 1, &l);