From 25d839ed10b67353ed0ae065b87935f2b4d2d83c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Mar 2017 10:55:55 -0700 Subject: [PATCH] fix bug in simplifier of bv2int over concatentations exposed by #948 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifier/bv_simplifier_plugin.cpp | 25 +++++++++++++++------ src/smt/theory_arith_core.h | 7 +++--- src/smt/theory_bv.cpp | 5 +++-- 3 files changed, 25 insertions(+), 12 deletions(-) diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp index 11ed1b9e0..a72e7e117 100644 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ b/src/ast/simplifier/bv_simplifier_plugin.cpp @@ -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); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 513cf36a4..785e0120f 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -40,7 +40,7 @@ namespace smt { template void theory_arith::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(m_found_underspecified_op)); m_found_underspecified_op = true; } @@ -395,6 +395,7 @@ namespace smt { template theory_var theory_arith::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 theory_var theory_arith::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 theory_var theory_arith::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()) { diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a886c8a1e..ae2aa95e2 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -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);