mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
remove unused experimental feature - diff
This commit is contained in:
parent
280887cc5a
commit
e1a00f4917
|
@ -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<builtin_name>& 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));
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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<sat::constraint_base> 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;
|
||||
|
||||
|
|
Loading…
Reference in a new issue