From c29cfa81aee0c68f5e6b3b4a393ddd35745a8229 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 May 2022 02:08:11 -0700 Subject: [PATCH] prep for max/min diff --- src/ast/array_decl_plugin.cpp | 20 ++++++++++++ src/ast/array_decl_plugin.h | 6 ++++ src/sat/smt/array_axioms.cpp | 52 ++++++++++++++++++++++++++++++- src/sat/smt/array_internalize.cpp | 11 ++++++- src/sat/smt/array_solver.h | 6 ++++ 5 files changed, 93 insertions(+), 2 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 0757902f5..8b8047dd7 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -527,6 +527,19 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return nullptr; } return mk_array_ext(arity, domain, parameters[0].get_int()); + case OP_ARRAY_MAXDIFF: + case OP_ARRAY_MINDIFF: { + if (num_parameters != 0) + m_manager->raise_exception("min/maxdiff don't take any parameters"); + if (arity != 2 || domain[0] != domain[1] || !is_array_sort(domain[0]) || 1 != get_array_arity(domain[0])) + m_manager->raise_exception("min/maxdiff don't take two arrays of same sort and with integer index"); + sort* idx = get_array_domain(domain[0], 0); + arith_util arith(*m_manager); + if (!arith.is_int(domain[0])) + m_manager->raise_exception("min/maxdiff take integer index domain"); + return m_manager->mk_func_decl(k == OP_ARRAY_MAXDIFF ? symbol("maxdiff") : symbol("mindiff"), + arity, domain, arith.mk_int(), func_decl_info(m_family_id, k)); + } case OP_ARRAY_DEFAULT: return mk_default(arity, domain); case OP_SET_UNION: @@ -587,6 +600,13 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("subset",OP_SET_SUBSET)); op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT)); + +#if 0 +// not exposed + op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF)); + op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF)); +#endif + #if 0 op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE)); op_names.push_back(builtin_name("card", OP_SET_CARD)); diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 5a606a509..dd8443025 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -45,6 +45,8 @@ enum array_op_kind { OP_ARRAY_EXT, OP_ARRAY_DEFAULT, OP_ARRAY_MAP, + OP_ARRAY_MAXDIFF, + OP_ARRAY_MINDIFF, OP_SET_UNION, OP_SET_INTERSECT, OP_SET_DIFFERENCE, @@ -157,6 +159,8 @@ public: bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); } bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); } bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); } + bool is_maxdiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAXDIFF); } + bool is_mindiff(expr const* n) const { return is_app_of(n, m_fid, OP_ARRAY_MINDIFF); } bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); } bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); } bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); } @@ -182,6 +186,8 @@ public: bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value); MATCH_BINARY(is_subset); + MATCH_BINARY(is_maxdiff); + MATCH_BINARY(is_mindiff); }; class array_util : public array_recognizers { diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 84b12cf7d..40be702b1 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -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); } diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index e1d0d4b33..a83bce1e9 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -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; diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 511f971a3..4ad27842b 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -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 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);