mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

#5641 add handlers for basic set operations to euf=true

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-01 20:33:17 -08:00
parent 9d3c8a6a2f
commit 8245935d41
5 changed files with 69 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/ast/array_decl_plugin.h
View file

@ -150,6 +150,10 @@ public:
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
bool is_ext(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_EXT); }
bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_SET_UNION); }
bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_SET_INTERSECT); }
bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_SET_DIFFERENCE); }
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_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
@ -158,11 +162,14 @@ public:
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); }
bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); }
bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
func_decl * get_as_array_func_decl(expr * n) const;
func_decl * get_as_array_func_decl(func_decl* f) const;
@ -172,6 +179,8 @@ public:
bool is_const(expr* e, expr*& v) const;
bool is_store_ext(expr* e, expr_ref& a, expr_ref_vector& args, expr_ref& value);
MATCH_BINARY(is_subset);
};
class array_util : public array_recognizers {

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

@ -84,7 +84,7 @@ namespace array {
return assert_default_const_axiom(to_app(child));
else if (a.is_store(child))
return assert_default_store_axiom(to_app(child));
else if (a.is_map(child))
else if (is_map_combinator(child))
return assert_default_map_axiom(to_app(child));
else
return false;
@ -115,7 +115,7 @@ namespace array {
return assert_select_as_array_axiom(select, to_app(child));
else if (a.is_store(child))
return assert_select_store_axiom(select, to_app(child));
else if (a.is_map(child))
else if (is_map_combinator(child))
return assert_select_map_axiom(select, to_app(child));
else if (is_lambda(child))
return assert_select_lambda_axiom(select, child);
@ -273,16 +273,19 @@ namespace array {
return add_clause(lit1, ~lit2);
}
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);
}
/**
* Assert axiom:
* select(map[f](a, ... d), i) = f(select(a,i),...,select(d,i))
*/
bool solver::assert_select_map_axiom(app* select, app* map) {
++m_stats.m_num_select_map_axiom;
SASSERT(a.is_map(map));
SASSERT(a.is_select(select));
SASSERT(is_map_combinator(map));
SASSERT(map->get_num_args() > 0);
func_decl* f = a.get_map_func_decl(map);
unsigned num_args = select->get_num_args();
ptr_buffer<expr> args1, args2;
vector<ptr_vector<expr> > args2l;
@ -303,7 +306,8 @@ namespace array {
expr_ref sel1(m), sel2(m);
sel1 = a.mk_select(args1);
sel2 = m.mk_app(f, args2);
sel2 = apply_map(map, args2.size(), args2.data());
rewrite(sel2);
euf::enode* n1 = e_internalize(sel1);
euf::enode* n2 = e_internalize(sel2);
@ -330,21 +334,44 @@ namespace array {
return ctx.propagate(n1, n2, array_axiom());
}
expr_ref solver::apply_map(app* map, unsigned n, expr* const* args) {
expr_ref result(m);
if (a.is_map(map))
result = m.mk_app(a.get_map_func_decl(map), n, args);
else if (a.is_union(map))
result = m.mk_or(n, args);
else if (a.is_intersect(map))
result = m.mk_and(n, args);
else if (a.is_difference(map)) {
SASSERT(n > 0);
result = args[0];
for (unsigned i = 1; i < n; ++i)
result = m.mk_and(result, m.mk_not(args[i]));
}
else if (a.is_complement(map)) {
SASSERT(n == 1);
result = m.mk_not(args[0]);
}
else {
UNREACHABLE();
}
rewrite(result);
return result;
}
/**
* Assert:
* default(map[f](a,..,d)) = f(default(a),..,default(d))
*/
bool solver::assert_default_map_axiom(app* map) {
++m_stats.m_num_default_map_axiom;
SASSERT(a.is_map(map));
func_decl* f = a.get_map_func_decl(map);
SASSERT(map->get_num_args() == f->get_arity());
SASSERT(is_map_combinator(map));
expr_ref_vector args2(m);
for (expr* arg : *map)
args2.push_back(a.mk_default(arg));
expr_ref def1(a.mk_default(map), m);
expr_ref def2(m.mk_app(f, args2), m);
rewrite(def2);
expr_ref def2 = apply_map(map, args2.size(), args2.data());
return ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom());
}

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

@ -117,15 +117,24 @@ namespace array {
add_parent_default(find(n->get_arg(0)), n);
break;
case OP_ARRAY_MAP:
for (auto* arg : euf::enode_args(n))
add_parent_lambda(find(arg), n);
internalize_lambda_eh(n);
break;
case OP_SET_UNION:
case OP_SET_INTERSECT:
case OP_SET_DIFFERENCE:
case OP_SET_COMPLEMENT:
case OP_SET_SUBSET:
for (auto* arg : euf::enode_args(n))
add_parent_lambda(find(arg), n);
internalize_lambda_eh(n);
break;
case OP_SET_SUBSET: {
expr* x, *y;
VERIFY(a.is_subset(n->get_expr(), x, y));
expr_ref diff(a.mk_setminus(x, y), m);
expr_ref emp(a.mk_empty_set(x->get_sort()), m);
sat::literal eq = eq_internalize(diff, emp);
sat::literal sub = expr2literal(n->get_expr());
add_equiv(eq, sub);
break;
}
case OP_SET_HAS_SIZE:
case OP_SET_CARD:
ctx.unhandled_function(n->get_decl());
@ -163,15 +172,16 @@ namespace array {
set_prop_upward(find(n->get_arg(0)));
break;
case OP_ARRAY_MAP:
for (auto* arg : euf::enode_args(n))
set_prop_upward_store(arg);
set_prop_upward(find(n));
break;
case OP_SET_UNION:
case OP_SET_INTERSECT:
case OP_SET_DIFFERENCE:
case OP_SET_COMPLEMENT:
for (auto* arg : euf::enode_args(n))
set_prop_upward_store(arg);
set_prop_upward(find(n));
break;
case OP_SET_SUBSET:
break;
case OP_SET_HAS_SIZE:
case OP_SET_CARD:
ctx.unhandled_function(n->get_decl());

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

@ -275,6 +275,6 @@ namespace array {
}
bool solver::can_beta_reduce(expr* c) const {
return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || a.is_map(c);
return a.is_const(c) || a.is_as_array(c) || a.is_store(c) || is_lambda(c) || is_map_combinator(c);
}
}

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

@ -181,7 +181,9 @@ namespace array {
bool assert_congruent_axiom(expr* e1, expr* e2);
bool add_delayed_axioms();
bool add_as_array_eqs(euf::enode* n);
expr_ref apply_map(app* map, unsigned n, expr* const* args);
bool is_map_combinator(expr* e) const;
bool has_unitary_domain(app* array_term);
bool has_large_domain(expr* array_term);
std::pair<app*, func_decl*> mk_epsilon(sort* s);