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

add min/max diff in final check

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-04 07:39:38 -07:00
parent c29cfa81ae
commit 367bfedab0
6 changed files with 77 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -68,6 +68,8 @@ namespace array {
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_diffselect:
return assert_diff_select(r.n->get_app(), r.select->get_app());
case axiom_record::kind_t::is_congruence:
return assert_congruent_axiom(r.n->get_expr(), r.select->get_expr());
default:
@ -294,7 +296,7 @@ namespace array {
* 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) {
bool solver::assert_diff_select(app* md, app* ai) {
SASSERT(a.is_select(ai));
SASSERT(ai->get_num_args() == 2);
expr* A = ai->get_arg(0);
@ -303,7 +305,7 @@ namespace array {
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));
literal ineq = mk_literal(a.is_maxdiff(md) ? autil.mk_le(i, md) : autil.mk_le(md, i));
bool is_new = false;
if (ctx.get_enode(A)->get_root() == ctx.get_enode(B)->get_root()) {
literal eq_ab = eq_internalize(A, B);
@ -714,5 +716,26 @@ namespace array {
return false;
}
bool solver::add_diff_select_axioms() {
bool added = false;
auto add_diff_select = [&](euf::enode* md, euf::enode* a) {
var_data const& d = get_var_data(find(get_th_var(a)));
for (euf::enode* select : d.m_parent_selects) {
if (assert_diff_select(md->get_app(), select->get_app()))
added = true;
}
};
for (euf::enode* md : m_minmaxdiffs) {
euf::enode* a = md->get_arg(0);
euf::enode* b = md->get_arg(1);
add_diff_select(md, a);
add_diff_select(md, b);
}
return added;
}
}

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

@ -118,6 +118,8 @@ namespace array {
case OP_ARRAY_MINDIFF:
case OP_ARRAY_MAXDIFF:
push_axiom(diff_axiom(n));
m_minmaxdiffs.push_back(n);
ctx.push(push_back_vector(m_minmaxdiffs));
break;
case OP_ARRAY_DEFAULT:
add_parent_default(find(n->get_arg(0)), n);

7
src/sat/smt/array_solver.cpp
View file

@ -101,9 +101,14 @@ namespace array {
else if (!turn[idx] && add_interface_equalities())
return sat::check_result::CR_CONTINUE;
}
if (m_delay_qhead < m_axiom_trail.size())
if (add_diff_select_axioms())
return sat::check_result::CR_CONTINUE;
if (m_delay_qhead < m_axiom_trail.size())
return sat::check_result::CR_CONTINUE;
// validate_check();
return sat::check_result::CR_DONE;
}

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

@ -147,9 +147,9 @@ namespace array {
axiom_record::eq m_eq;
axiom_table_t m_axioms;
svector<axiom_record> m_axiom_trail;
unsigned m_qhead { 0 };
unsigned m_delay_qhead { 0 };
bool m_enable_delay { true };
unsigned m_qhead = 0;
unsigned m_delay_qhead = 0;
bool m_enable_delay = true;
struct reset_new;
void push_axiom(axiom_record const& r);
bool propagate_axiom(unsigned idx);
@ -166,7 +166,8 @@ namespace array {
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); }
euf::enode_vector m_minmaxdiffs;
axiom_record diff_select_axiom(euf::enode* md, euf::enode* ai) { return axiom_record(axiom_record::kind_t::is_diffselect, md, ai); }
scoped_ptr<sat::constraint_base> m_constraint;
@ -187,6 +188,7 @@ namespace array {
bool assert_congruent_axiom(expr* e1, expr* e2);
bool add_delayed_axioms();
bool add_as_array_eqs(euf::enode* n);
bool add_diff_select_axioms();
expr_ref apply_map(app* map, unsigned n, expr* const* args);
bool is_map_combinator(expr* e) const;