mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

(mev) only reduce function interpretation

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-21 22:59:52 -04:00
parent 493a3a6312
commit 972ab6298c
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/model/model_evaluator.cpp
View file

@ -432,6 +432,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
func_interp* g = m_model.get_func_interp(f); func_interp* g = m_model.get_func_interp(f);
unsigned sz = g->num_entries(); unsigned sz = g->num_entries();
unsigned arity = f->get_arity(); unsigned arity = f->get_arity();
unsigned base_sz = stores.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr_ref_vector store(m()); expr_ref_vector store(m());
func_entry const* fe = g->get_entry(i); func_entry const* fe = g->get_entry(i);
@ -456,7 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";); TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << else_case << "\n";);
return false; return false;
} }
for (unsigned i = stores.size(); are_values && i > 0; ) { for (unsigned i = stores.size(); are_values && i > base_sz; ) {
--i; --i;
if (m().are_equal(else_case, stores[i].back())) { if (m().are_equal(else_case, stores[i].back())) {
for (unsigned j = i + 1; j < stores.size(); ++j) { for (unsigned j = i + 1; j < stores.size(); ++j) {