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

Add initial implementation of bit-vector SLS evaluation module in bv_sls_eval.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-01 16:53:44 -07:00
parent 27e3d28cfc
commit 027dd9cfd8
3 changed files with 1996 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

1995
src/ast/sls/bv_sls_eval.cpp Normal file
View file

File diff suppressed because it is too large Load diff

1
src/ast/sls/sls_bv_eval.cpp
View file

@ -1838,7 +1838,6 @@ namespace sls {
auto& ve = assign_value(e);
for (unsigned j = e->get_num_args() - 1; j > idx; --j)
bw += bv.get_bv_size(e->get_arg(j));
//verbose_stream() << m_bounded_pp(e, m) << " " << idx << " " << bw << "\n";
auto& a = wval(e, idx);
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, ve.get(i + bw));

5
src/ast/sls/sls_bv_terms.cpp
View file

@ -47,10 +47,7 @@ namespace sls {
for (unsigned i = 1; i < num_args; ++i)\
r = oper(r, arg(i)); \
if (bv.is_concat(e)) {
FOLD_OP(bv.mk_concat);
}
else if (bv.is_bv_sdiv(e) || bv.is_bv_sdiv0(e) || bv.is_bv_sdivi(e)) {
if (bv.is_bv_sdiv(e) || bv.is_bv_sdiv0(e) || bv.is_bv_sdivi(e)) {
r = mk_sdiv(arg(0), arg(1));
}
else if (bv.is_bv_smod(e) || bv.is_bv_smod0(e) || bv.is_bv_smodi(e)) {