diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index f986eb46a..0800b6af3 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -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 { diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index b4ab89d1f..296c35b8c 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -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 args1, args2; vector > 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()); } diff --git a/src/sat/smt/array_internalize.cpp b/src/sat/smt/array_internalize.cpp index 5e285112d..b7b79ddbc 100644 --- a/src/sat/smt/array_internalize.cpp +++ b/src/sat/smt/array_internalize.cpp @@ -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()); diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp index f3414a4c6..f2836d9aa 100644 --- a/src/sat/smt/array_solver.cpp +++ b/src/sat/smt/array_solver.cpp @@ -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); } } diff --git a/src/sat/smt/array_solver.h b/src/sat/smt/array_solver.h index dbcbb36df..1c2935c99 100644 --- a/src/sat/smt/array_solver.h +++ b/src/sat/smt/array_solver.h @@ -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 mk_epsilon(sort* s);