mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

compress store array before model-eval rewriter sees it

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-27 16:55:07 -08:00
parent fe1622b592
commit 72ae161307
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/sls/sls_array_plugin.cpp
View file

@ -394,11 +394,16 @@ namespace sls {
// TODO: adapt to handle "const" arrays and multi-dimensional arrays. // TODO: adapt to handle "const" arrays and multi-dimensional arrays.
auto& kv = *m_kv; auto& kv = *m_kv;
auto n = m_g->find(e)->get_root(); auto n = m_g->find(e)->get_root();
expr_ref r(n->get_expr(), m); expr_ref r(n->get_expr(), m), key(m);
expr_mark visited;
for (auto [k, v] : kv[n]) { for (auto [k, v] : kv[n]) {
ptr_vector<expr> args; ptr_vector<expr> args;
key = ctx.get_value(k.sel->get_arg(1)->get_expr());
if (visited.is_marked(key))
continue;
visited.mark(key);
args.push_back(r); args.push_back(r);
args.push_back(k.sel->get_arg(1)->get_expr()); args.push_back(key);
args.push_back(v->get_expr()); args.push_back(v->get_expr());
r = a.mk_store(args); r = a.mk_store(args);
} }

2
src/model/model_evaluator.cpp
View file

@ -89,7 +89,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
m_fpau(m), m_fpau(m),
m_dt(m), m_dt(m),
m_pinned(m) { m_pinned(m) {
bool flat = true; bool flat = false;
m_b_rw.set_flat_and_or(flat); m_b_rw.set_flat_and_or(flat);
m_a_rw.set_flat(flat); m_a_rw.set_flat(flat);
m_bv_rw.set_flat(flat); m_bv_rw.set_flat(flat);