mirror of
https://github.com/Z3Prover/z3
synced 2025-06-21 21:33:39 +00:00
model_evaluator: optionally expand arrays as sequence of stores
commit on behalf of Nikolaj
This commit is contained in:
parent
2f369d8d41
commit
7281616084
3 changed files with 26 additions and 18 deletions
|
@ -53,6 +53,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
bool m_model_completion;
|
bool m_model_completion;
|
||||||
bool m_cache;
|
bool m_cache;
|
||||||
bool m_array_equalities;
|
bool m_array_equalities;
|
||||||
|
bool m_array_as_stores;
|
||||||
|
|
||||||
evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
|
evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
|
||||||
m(m),
|
m(m),
|
||||||
|
@ -87,6 +88,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
m_model_completion = p.completion();
|
m_model_completion = p.completion();
|
||||||
m_cache = p.cache();
|
m_cache = p.cache();
|
||||||
m_array_equalities = p.array_equalities();
|
m_array_equalities = p.array_equalities();
|
||||||
|
m_array_as_stores = p.array_as_stores();
|
||||||
}
|
}
|
||||||
|
|
||||||
bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
bool evaluate(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||||
|
@ -196,20 +198,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
|
if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
|
||||||
return BR_REWRITE1;
|
return BR_REWRITE1;
|
||||||
}
|
}
|
||||||
|
if (false && m_array_as_stores && m_ar.is_array(result)) {
|
||||||
|
expand_stores(result);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
|
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
|
||||||
return st;
|
return st;
|
||||||
}
|
}
|
||||||
|
|
||||||
void expand_value(expr_ref& val) {
|
void expand_stores(expr_ref& val) {
|
||||||
vector<expr_ref_vector> stores;
|
vector<expr_ref_vector> stores;
|
||||||
expr_ref else_case(m);
|
expr_ref else_case(m);
|
||||||
bool _unused;
|
bool _unused;
|
||||||
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
|
if (m_ar.is_array(val) && extract_array_func_interp(val, stores, else_case, _unused)) {
|
||||||
sort* srt = m.get_sort(val);
|
sort* srt = m.get_sort(val);
|
||||||
val = m_ar.mk_const_array(srt, else_case);
|
val = m_ar.mk_const_array(srt, else_case);
|
||||||
for (unsigned i = stores.size(); i > 0; ) {
|
for (unsigned i = stores.size(); i-- > 0; ) {
|
||||||
--i;
|
|
||||||
expr_ref_vector args(m);
|
expr_ref_vector args(m);
|
||||||
args.push_back(val);
|
args.push_back(val);
|
||||||
args.append(stores[i].size(), stores[i].c_ptr());
|
args.append(stores[i].size(), stores[i].c_ptr());
|
||||||
|
@ -288,7 +292,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
|
|
||||||
bool cache_results() const { return m_cache; }
|
bool cache_results() const { return m_cache; }
|
||||||
|
|
||||||
|
|
||||||
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
|
br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
|
||||||
if (a == b) {
|
if (a == b) {
|
||||||
result = m.mk_true();
|
result = m.mk_true();
|
||||||
|
@ -497,9 +500,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
|
||||||
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
|
TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m) << "\n";);
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
};
|
};
|
||||||
|
|
||||||
template class rewriter_tpl<evaluator_cfg>;
|
template class rewriter_tpl<evaluator_cfg>;
|
||||||
|
@ -513,10 +513,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
|
||||||
m_cfg(md.get_manager(), md, p) {
|
m_cfg(md.get_manager(), md, p) {
|
||||||
set_cancel_check(false);
|
set_cancel_check(false);
|
||||||
}
|
}
|
||||||
|
void expand_stores(expr_ref &val) {m_cfg.expand_stores(val);}
|
||||||
void expand_value (expr_ref &val) {
|
|
||||||
m_cfg.expand_value (val);
|
|
||||||
}
|
|
||||||
};
|
};
|
||||||
|
|
||||||
model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
|
model_evaluator::model_evaluator(model_core & md, params_ref const & p) {
|
||||||
|
@ -571,7 +568,7 @@ void model_evaluator::reset(model_core &model, params_ref const& p) {
|
||||||
void model_evaluator::operator()(expr * t, expr_ref & result) {
|
void model_evaluator::operator()(expr * t, expr_ref & result) {
|
||||||
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
|
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
|
||||||
m_imp->operator()(t, result);
|
m_imp->operator()(t, result);
|
||||||
m_imp->expand_value(result);
|
m_imp->expand_stores(result);
|
||||||
}
|
}
|
||||||
|
|
||||||
expr_ref model_evaluator::operator()(expr * t) {
|
expr_ref model_evaluator::operator()(expr * t) {
|
||||||
|
@ -581,6 +578,13 @@ expr_ref model_evaluator::operator()(expr * t) {
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
expr_ref_vector model_evaluator::operator()(expr_ref_vector const& ts) {
|
||||||
|
expr_ref_vector rs(m());
|
||||||
|
for (expr* t : ts) rs.push_back((*this)(t));
|
||||||
|
return rs;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
bool model_evaluator::is_true(expr* t) {
|
bool model_evaluator::is_true(expr* t) {
|
||||||
expr_ref tmp(m());
|
expr_ref tmp(m());
|
||||||
return eval(t, tmp, true) && m().is_true(tmp);
|
return eval(t, tmp, true) && m().is_true(tmp);
|
||||||
|
@ -614,6 +618,3 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
|
||||||
tmp = mk_and(ts);
|
tmp = mk_and(ts);
|
||||||
return eval(tmp, r, model_completion);
|
return eval(tmp, r, model_completion);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -44,6 +44,7 @@ public:
|
||||||
|
|
||||||
void operator()(expr * t, expr_ref & r);
|
void operator()(expr * t, expr_ref & r);
|
||||||
expr_ref operator()(expr* t);
|
expr_ref operator()(expr* t);
|
||||||
|
expr_ref_vector operator()(expr_ref_vector const& ts);
|
||||||
|
|
||||||
// exception safe
|
// exception safe
|
||||||
bool eval(expr* t, expr_ref& r, bool model_completion = true);
|
bool eval(expr* t, expr_ref& r, bool model_completion = true);
|
||||||
|
@ -53,6 +54,11 @@ public:
|
||||||
bool is_false(expr * t);
|
bool is_false(expr * t);
|
||||||
bool is_true(expr_ref_vector const& ts);
|
bool is_true(expr_ref_vector const& ts);
|
||||||
|
|
||||||
|
/**
|
||||||
|
* best effort evaluator of extensional array equality.
|
||||||
|
*/
|
||||||
|
expr_ref eval_array_eq(app* e, expr* arg1, expr* arg2);
|
||||||
|
|
||||||
void cleanup(params_ref const & p = params_ref());
|
void cleanup(params_ref const & p = params_ref());
|
||||||
void reset(params_ref const & p = params_ref());
|
void reset(params_ref const & p = params_ref());
|
||||||
void reset(model_core& model, params_ref const & p = params_ref());
|
void reset(model_core& model, params_ref const & p = params_ref());
|
||||||
|
|
|
@ -4,6 +4,7 @@ def_module_params('model_evaluator',
|
||||||
max_steps_param(),
|
max_steps_param(),
|
||||||
('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
|
('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
|
||||||
('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
|
('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
|
||||||
('array_equalities', BOOL, True, 'evaluate array equalities')
|
('array_equalities', BOOL, True, 'evaluate array equalities'),
|
||||||
|
('array_as_stores', BOOL, True, 'return array as a set of stores'),
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue