mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

prep for max/min diff

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-05-04 02:08:11 -07:00
parent 87d2a3b4e5
commit c29cfa81ae
5 changed files with 93 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/sat/smt/array_axioms.cpp
View file

@ -59,13 +59,15 @@ namespace array {
axiom_record& r = m_axiom_trail[idx];
switch (r.m_kind) {
case axiom_record::kind_t::is_store:
return assert_store_axiom(to_app(r.n->get_expr()));
return assert_store_axiom(r.n->get_app());
case axiom_record::kind_t::is_select:
return assert_select(idx, r);
case axiom_record::kind_t::is_default:
return assert_default(r);
case axiom_record::kind_t::is_extensionality:
return assert_extensionality(r.n->get_expr(), r.select->get_expr());
case axiom_record::kind_t::is_diff:
return assert_diff(r.n->get_app());
case axiom_record::kind_t::is_congruence:
return assert_congruent_axiom(r.n->get_expr(), r.select->get_expr());
default:
@ -273,6 +275,54 @@ namespace array {
return add_clause(lit1, ~lit2);
}
/**
* a = b or default(a) != default(b) or a[md(a,b)] != b[md(a,b)]
*/
bool solver::assert_diff(expr* md) {
expr* x, *y;
SASSERT(a.is_maxdiff(md, x, y) || a.is_mindiff(md, x, y));
expr* args1[2] = { x, md };
expr* args2[2] = { y, md };
literal eq = eq_internalize(x, y);
literal eq_default = eq_internalize(a.mk_default(x), a.mk_default(y));
literal eq_md = eq_internalize(a.mk_select(2, args1), a.mk_select(2, args2));
return add_clause(eq, ~eq_default, ~eq_md);
}
/**
* a = b and a[i] != c[i] => i <= md(b, c) or default(b) != default(c)
* a = c and a[i] != b[i] => i <= md(b, c) or default(b) != default(c)
* where ai = a[i], md = md(b, c)
*/
bool solver::assert_diff_select(app* ai, app* md) {
SASSERT(a.is_select(ai));
SASSERT(ai->get_num_args() == 2);
expr* A = ai->get_arg(0);
expr* i = ai->get_arg(1);
expr* B = md->get_arg(0);
expr* C = md->get_arg(1);
literal eq_default = eq_internalize(a.mk_default(B), a.mk_default(C));
arith_util autil(m);
literal ineq = mk_literal(autil.mk_le(i, md));
bool is_new = false;
if (ctx.get_enode(A)->get_root() == ctx.get_enode(B)->get_root()) {
literal eq_ab = eq_internalize(A, B);
expr* args[2] = { C, i };
literal eq_select = eq_internalize(ai, a.mk_select(2, args));
if (add_clause(~eq_ab, eq_select, ineq, ~eq_default))
is_new = true;
}
if (ctx.get_enode(A)->get_root() == ctx.get_enode(C)->get_root()) {
literal eq_ac = eq_internalize(A, C);
expr* args[2] = { B, i };
literal eq_select = eq_internalize(ai, a.mk_select(2, args));
if (add_clause(~eq_ac, eq_select, ineq, ~eq_default))
is_new = true;
}
return is_new;
}
bool solver::is_map_combinator(expr* map) const {
return a.is_map(map) || a.is_union(map) || a.is_intersect(map) || a.is_difference(map) || a.is_complement(map);
}

11
src/sat/smt/array_internalize.cpp
View file

@ -99,7 +99,8 @@ namespace array {
}
void solver::internalize_eh(euf::enode* n) {
switch (n->get_decl()->get_decl_kind()) {
auto k = n->get_decl()->get_decl_kind();
switch (k) {
case OP_STORE:
ctx.push_vec(get_var_data(find(n)).m_lambdas, n);
push_axiom(store_axiom(n));
@ -114,6 +115,10 @@ namespace array {
SASSERT(is_array(n->get_arg(0)));
push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
break;
case OP_ARRAY_MINDIFF:
case OP_ARRAY_MAXDIFF:
push_axiom(diff_axiom(n));
break;
case OP_ARRAY_DEFAULT:
add_parent_default(find(n->get_arg(0)), n);
break;
@ -169,6 +174,10 @@ namespace array {
break;
case OP_ARRAY_EXT:
break;
case OP_ARRAY_MINDIFF:
case OP_ARRAY_MAXDIFF:
// todo
break;
case OP_ARRAY_DEFAULT:
set_prop_upward(find(n->get_arg(0)));
break;

6
src/sat/smt/array_solver.h
View file

@ -83,6 +83,8 @@ namespace array {
is_store,
is_select,
is_extensionality,
is_diff,
is_diffselect,
is_default,
is_congruence
};
@ -163,6 +165,8 @@ namespace array {
axiom_record store_axiom(euf::enode* n) { return axiom_record(axiom_record::kind_t::is_store, n); }
axiom_record extensionality_axiom(euf::enode* x, euf::enode* y) { return axiom_record(axiom_record::kind_t::is_extensionality, x, y); }
axiom_record congruence_axiom(euf::enode* a, euf::enode* b) { return axiom_record(axiom_record::kind_t::is_congruence, a, b); }
axiom_record diff_axiom(euf::enode* md) { return axiom_record(axiom_record::kind_t::is_diff, md); }
axiom_record diff_select_axiom(euf::enode* ai, euf::enode* md) { return axiom_record(axiom_record::kind_t::is_diffselect, ai, md); }
scoped_ptr<sat::constraint_base> m_constraint;
@ -175,6 +179,8 @@ namespace array {
bool assert_select_map_axiom(app* select, app* map);
bool assert_select_lambda_axiom(app* select, expr* lambda);
bool assert_extensionality(expr* e1, expr* e2);
bool assert_diff(expr* md);
bool assert_diff_select(app* ai, app* md);
bool assert_default_map_axiom(app* map);
bool assert_default_const_axiom(app* cnst);
bool assert_default_store_axiom(app* store);