From e1a00f4917535e1edbdd212a20530051216120e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Oct 2022 16:13:24 -0700 Subject: [PATCH] remove unused experimental feature - diff --- src/ast/array_decl_plugin.cpp | 16 ------- src/ast/array_decl_plugin.h | 6 --- src/sat/smt/array_axioms.cpp | 73 ------------------------------- src/sat/smt/array_internalize.cpp | 10 ----- src/sat/smt/array_solver.cpp | 3 -- src/sat/smt/array_solver.h | 10 +---- 6 files changed, 1 insertion(+), 117 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 5e9356865..7c2b357c2 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -529,19 +529,6 @@ 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(idx)) - 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: @@ -603,9 +590,6 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT)); - op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF)); - op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF)); - #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 fdad692ac..83d541097 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -45,8 +45,6 @@ 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, @@ -161,8 +159,6 @@ 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); } @@ -189,8 +185,6 @@ 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 901344293..ff60bf675 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -66,10 +66,6 @@ namespace array { 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_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: @@ -278,54 +274,6 @@ 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 = nullptr, *y = nullptr; - VERIFY(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* md, app* ai) { - 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(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); - 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); } @@ -738,26 +686,5 @@ 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; - } - - - } diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index c7517f5a4..d5a1dd2c5 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -115,12 +115,6 @@ 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)); - 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))); break; @@ -176,10 +170,6 @@ 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.cpp b/src/sat/smt/array_solver.cpp index 2d3d13d3a..7a8f31f1e 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -101,9 +101,6 @@ namespace array { else if (!turn[idx] && add_interface_equalities()) return sat::check_result::CR_CONTINUE; } - - 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; diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index 4f100d694..c63eedaca 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -84,8 +84,6 @@ namespace array { is_store, is_select, is_extensionality, - is_diff, - is_diffselect, is_default, is_congruence }; @@ -95,7 +93,7 @@ namespace array { is_applied }; kind_t m_kind; - state_t m_state { state_t::is_new }; + state_t m_state = state_t::is_new; euf::enode* n; euf::enode* select; axiom_record(kind_t k, euf::enode* n, euf::enode* select = nullptr) : m_kind(k), n(n), select(select) {} @@ -166,9 +164,6 @@ 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); } - 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 m_constraint; @@ -181,15 +176,12 @@ 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); 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;