mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Correctly report unsupported features in bvarray2uf_rewriter. Fixes #4046 and #4047.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-07-15 16:16:29 +00:00
parent 7dd28708a1
commit c321fb7726
No known key found for this signature in database
GPG key ID: BCF6360F86294467
2 changed files with 11 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/tactic/bv/bvarray2uf_rewriter.cpp
View file

@ -112,12 +112,11 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
sort * range = get_value_sort(e);
bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " new func_decl is " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
if (is_uninterp_const(e)) {
if (m_fmc)
m_fmc->add(e, m_array_util.mk_as_array(bv_f));
if (m_fmc) {
m_fmc->hide(bv_f);
if (is_uninterp_const(e))
m_fmc->add(e, m_array_util.mk_as_array(bv_f));
}
else if (m_fmc)
m_fmc->hide(bv_f);
m_arrays_fs.insert(e, bv_f);
m_manager.inc_ref(e);
m_manager.inc_ref(bv_f);
@ -181,22 +180,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
func_decl_ref itefd(m_manager);
e = m_manager.mk_ite(c, f_ta, f_fa);
func_decl * bv_f = nullptr;
if (!m_arrays_fs.find(f_a, bv_f)) {
sort * domain = get_index_sort(args[1]);
sort * range = get_value_sort(args[1]);
bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
TRACE("bvarray2uf_rw", tout << mk_ismt2_pp(e, m_manager) << " -> " << bv_f->get_name() << std::endl; );
if (is_uninterp_const(e)) {
if (m_fmc)
m_fmc->add(e, m_array_util.mk_as_array(bv_f));
}
else if (m_fmc)
m_fmc->hide(bv_f);
m_arrays_fs.insert(e, bv_f);
m_manager.inc_ref(e);
m_manager.inc_ref(bv_f);
}
func_decl * bv_f = mk_uf_for_array(e);
expr_ref q(m_manager), body(m_manager);
body = m_manager.mk_eq(m_manager.mk_app(bv_f, x), e);
@ -207,7 +191,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
TRACE("bvarray2uf_rw", tout << "result: " << mk_ismt2_pp(result, m_manager) << ")" << std::endl;);
res = BR_DONE;
}
else if (f->get_family_id() == m_manager.get_basic_family_id() && is_bv_array(f->get_range())) {
throw default_exception("not handled by bvarray2uf");
@ -252,7 +236,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
" index: " << mk_ismt2_pp(i, m()) << std::endl;);
if (!is_bv_array(t))
res = BR_FAILED;
throw default_exception("not handled by bvarray2uf");
else {
// From [1]: Then, we replace terms of the form select(t, i) with f_t(i).
func_decl_ref f_t(mk_uf_for_array(t), m_manager);
@ -262,7 +246,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
}
else {
if (!is_bv_array(f->get_range()))
res = BR_FAILED;
throw default_exception("not handled by bvarray2uf");
else {
if (m_array_util.is_const(f)) {
SASSERT(num == 1);
@ -330,7 +314,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
" index: " << mk_ismt2_pp(i, m()) <<
" value: " << mk_ismt2_pp(v, m()) << std::endl;);
if (!is_bv_array(s))
res = BR_FAILED;
throw default_exception("not handled by bvarray2uf");
else {
expr_ref t(m_manager.mk_app(f, num, args), m_manager);
// From [1]: For every term t of the form store(s, i, v), we add the universal
@ -361,7 +345,6 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
}
else {
throw default_exception("not handled by bvarray2uf");
// res = BR_FAILED;
}
}
}

2
src/tactic/bv/bvarray2uf_tactic.cpp
View file

@ -54,6 +54,8 @@ class bvarray2uf_tactic : public tactic {
tactic_report report("bvarray2uf", *g);
result.reset();
fail_if_unsat_core_generation("bvarray2uf", g);
// bvarray2uf_rewriter does not support proofs (yet).
fail_if_proof_generation("bvarray2uf", g);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();