mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
add rewriting option to simplify store equalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
5eed106ffe
commit
e35fd58968
|
@ -25,6 +25,7 @@ void array_rewriter::updt_params(params_ref const & _p) {
|
|||
array_rewriter_params p(_p);
|
||||
m_sort_store = p.sort_store();
|
||||
m_expand_select_store = p.expand_select_store();
|
||||
m_expand_store_eq = p.expand_store_eq();
|
||||
}
|
||||
|
||||
void array_rewriter::get_param_descrs(param_descrs & r) {
|
||||
|
@ -365,3 +366,40 @@ br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & res
|
|||
return BR_REWRITE3;
|
||||
}
|
||||
|
||||
br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
|
||||
if (!m_expand_store_eq) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
expr* lhs1 = lhs;
|
||||
while (m_util.is_store(lhs1)) {
|
||||
lhs1 = to_app(lhs1)->get_arg(0);
|
||||
}
|
||||
expr* rhs1 = rhs;
|
||||
while (m_util.is_store(rhs1)) {
|
||||
rhs1 = to_app(rhs1)->get_arg(0);
|
||||
}
|
||||
if (lhs1 != rhs1) {
|
||||
return BR_FAILED;
|
||||
}
|
||||
ptr_buffer<expr> fmls, args;
|
||||
expr* e;
|
||||
expr_ref tmp1(m()), tmp2(m());
|
||||
#define MK_EQ() \
|
||||
while (m_util.is_store(e)) { \
|
||||
args.push_back(lhs); \
|
||||
args.append(to_app(e)->get_num_args()-2,to_app(e)->get_args()+1); \
|
||||
mk_select(args.size(), args.c_ptr(), tmp1); \
|
||||
args[0] = rhs; \
|
||||
mk_select(args.size(), args.c_ptr(), tmp2); \
|
||||
fmls.push_back(m().mk_eq(tmp1, tmp2)); \
|
||||
e = to_app(e)->get_arg(0); \
|
||||
args.reset(); \
|
||||
} \
|
||||
|
||||
e = lhs;
|
||||
MK_EQ();
|
||||
e = rhs;
|
||||
MK_EQ();
|
||||
result = m().mk_and(fmls.size(), fmls.c_ptr());
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
|
|
|
@ -31,12 +31,14 @@ class array_rewriter {
|
|||
array_util m_util;
|
||||
bool m_sort_store;
|
||||
bool m_expand_select_store;
|
||||
bool m_expand_store_eq;
|
||||
template<bool CHECK_DISEQ>
|
||||
lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
|
||||
public:
|
||||
array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
|
||||
m_util(m) {
|
||||
updt_params(p);
|
||||
|
||||
}
|
||||
ast_manager & m() const { return m_util.get_manager(); }
|
||||
family_id get_fid() const { return m_util.get_family_id(); }
|
||||
|
@ -60,6 +62,7 @@ public:
|
|||
br_status mk_set_complement(expr * arg, expr_ref & result);
|
||||
br_status mk_set_difference(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_set_subset(expr * arg1, expr * arg2, expr_ref & result);
|
||||
br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -2,4 +2,5 @@ def_module_params(module_name='rewriter',
|
|||
class_name='array_rewriter_params',
|
||||
export=True,
|
||||
params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"),
|
||||
("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
|
||||
("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))
|
||||
|
|
|
@ -62,6 +62,8 @@ struct mk_simplified_app::imp {
|
|||
st = m_dt_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_f_rw.get_fid())
|
||||
st = m_f_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_ar_rw.get_fid())
|
||||
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
|
||||
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
|
|
|
@ -169,7 +169,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
|
|||
st = m_dt_rw.mk_eq_core(args[0], args[1], result);
|
||||
else if (s_fid == m_f_rw.get_fid())
|
||||
st = m_f_rw.mk_eq_core(args[0], args[1], result);
|
||||
|
||||
else if (s_fid == m_ar_rw.get_fid())
|
||||
st = m_ar_rw.mk_eq_core(args[0], args[1], result);
|
||||
|
||||
if (st != BR_FAILED)
|
||||
return st;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue