mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-04-09 16:51:42 -07:00
commit 6e57015a12
15 changed files with 648 additions and 141 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -25,6 +25,7 @@ Notes:
#include"ast_pp.h"
#include"bvarray2uf_rewriter.h"
#include"rewriter_def.h"
#include"ref_util.h"
// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
// Quantified Bit-Vector Formulas, in Formal Methods in System Design,
@ -50,10 +51,7 @@ bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref con
}
bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
it != m_arrays_fs.end();
it++)
m_manager.dec_ref(it->m_value);
dec_ref_map_key_values(m_manager, m_arrays_fs);
}
void bvarray2uf_rewriter_cfg::reset() {}
@ -110,12 +108,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
if (m_array_util.is_as_array(e))
return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
else {
app * a = to_app(e);
func_decl * bv_f = 0;
if (!m_arrays_fs.find(e, bv_f)) {
sort * domain = get_index_sort(a);
sort * range = get_value_sort(a);
sort * domain = get_index_sort(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_emc)
m_emc->insert(to_app(e)->get_decl(),
@ -124,8 +122,12 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
else if (m_fmc)
m_fmc->insert(bv_f);
m_arrays_fs.insert(e, bv_f);
m_manager.inc_ref(e);
m_manager.inc_ref(bv_f);
}
else {
TRACE("bvarray2uf_rw", tout << "for " << mk_ismt2_pp(e, m_manager) << " found " << mk_ismt2_pp(bv_f, m_manager) << std::endl; );
}
return func_decl_ref(bv_f, m_manager);
}
@ -138,18 +140,24 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
SASSERT(num == 2);
// From [1]: Finally, we replace equations of the form t = s,
// where t and s are arrays, with \forall x . f_t(x) = f_s(x).
func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
if (m_manager.are_equal(args[0], args[1])) {
result = m_manager.mk_true();
res = BR_DONE;
}
else {
func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
symbol names[1] = { symbol("x") };
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
symbol names[1] = { symbol("x") };
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
expr_ref body(m_manager);
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
expr_ref body(m_manager);
body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
result = m_manager.mk_forall(1, sorts, names, body);
res = BR_DONE;
result = m_manager.mk_forall(1, sorts, names, body);
res = BR_DONE;
}
}
else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
result = m_manager.mk_distinct_expanded(num, args);
@ -310,7 +318,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
}
}
CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
CTRACE("bvarray2uf_rw", res == BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
return res;
}

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

@ -62,7 +62,6 @@ class bvarray2uf_tactic : public tactic {
SASSERT(g->is_well_sorted());
tactic_report report("bvarray2uf", *g);
mc = 0; pc = 0; core = 0; result.reset();
fail_if_proof_generation("bvarray2uf", g);
fail_if_unsat_core_generation("bvarray2uf", g);
TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
@ -73,7 +72,6 @@ class bvarray2uf_tactic : public tactic {
filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
mc = concat(emc, fmc);
m_rw.set_mcs(emc, fmc);
}
@ -86,10 +84,10 @@ class bvarray2uf_tactic : public tactic {
break;
expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr);
//if (m_produce_proofs) {
// proof * pr = g->pr(idx);
// new_pr = m.mk_modus_ponens(pr, new_pr);
//}
if (m_produce_proofs) {
proof * pr = g->pr(idx);
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
}
g->update(idx, new_curr, new_pr, g->dep(idx));
}
@ -143,7 +141,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
std::swap(d, m_imp);
std::swap(d, m_imp);
dealloc(d);
}

44
src/tactic/extension_model_converter.cpp
View file

@ -43,41 +43,6 @@ static void display_decls_info(std::ostream & out, model_ref & md) {
}
}
bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args) {
args.reset();
if (!is_app(e) || !m().is_ite(to_app(e)))
return false;
app * a = to_app(e);
expr * c = a->get_arg(0);
expr * t = a->get_arg(1);
expr * f = a->get_arg(2);
if ((arity == 0) ||
(arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) ||
(arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity)))
return false;
args.resize(arity, 0);
for (unsigned i = 0; i < arity; i++) {
expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i);
if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2)
return false;
expr * a0 = to_app(ci)->get_arg(0);
expr * a1 = to_app(ci)->get_arg(1);
if (is_var(a0) && to_var(a0)->get_idx() == i)
args[i] = a1;
else if (is_var(a1) && to_var(a1)->get_idx() == i)
args[i] = a0;
else
return false;
}
return true;
}
void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
SASSERT(goal_idx == 0);
TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
@ -97,14 +62,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
}
else {
func_interp * new_fi = alloc(func_interp, m(), arity);
expr * e = val.get();
ptr_vector<expr> args;
while (is_fi_entry_expr(e, arity, args)) {
TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;);
new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1));
e = to_app(e)->get_arg(2);
}
new_fi->set_else(e);
new_fi->set_else(val);
md->register_decl(f, new_fi);
}
}

3
src/tactic/extension_model_converter.h
View file

@ -43,9 +43,6 @@ public:
void insert(func_decl * v, expr * def);
virtual model_converter * translate(ast_translation & translator);
private:
bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector<expr> & args);
};