mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

distribute concat over bvxor and bvor, #2470

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-09 10:03:21 -07:00
parent 8579a004d0
commit e2d91ce1fc
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/bv_rewriter.cpp
View file

@ -1928,10 +1928,10 @@ bool bv_rewriter::distribute_concat(decl_kind k, unsigned n, expr* const* args,
expr* e = to_app(arg)->get_arg(0); expr* e = to_app(arg)->get_arg(0);
unsigned sz1 = get_bv_size(e); unsigned sz1 = get_bv_size(e);
unsigned sz2 = get_bv_size(arg); unsigned sz2 = get_bv_size(arg);
ptr_buffer<expr> args1, args2; expr_ref_vector args1(m()), args2(m());
for (unsigned j = 0; j < n; ++j) { for (unsigned j = 0; j < n; ++j) {
args1.push_back(m_mk_extract(sz2-1, sz1, args[j])); args1.push_back(m_mk_extract(sz2 - 1, sz2 - sz1, args[j]));
args2.push_back(m_mk_extract(sz1-1,0, args[j])); args2.push_back(m_mk_extract(sz2 - sz1 - 1, 0, args[j]));
} }
expr* arg1 = m().mk_app(get_fid(), k, args1.size(), args1.c_ptr()); expr* arg1 = m().mk_app(get_fid(), k, args1.size(), args1.c_ptr());
expr* arg2 = m().mk_app(get_fid(), k, args2.size(), args2.c_ptr()); expr* arg2 = m().mk_app(get_fid(), k, args2.size(), args2.c_ptr());