diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index d48ce76e2..04d7793a0 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -580,7 +580,7 @@ extern "C" { expr* args[2] = { _t, _v }; sort* domain[2] = { m.get_sort(_t), m.get_sort(_v) }; parameter param(_f); - func_decl * d = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); + func_decl * d = m.mk_func_decl(mk_c(c)->get_dt_fid(), OP_DT_UPDATE_FIELD, 1, ¶m, 2, domain); app* r = m.mk_app(d, 2, args); mk_c(c)->save_ast_trail(r); check_sorts(c, r); diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 071a35af0..66cf0e742 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -30,8 +30,8 @@ array_decl_plugin::array_decl_plugin(): m_default_sym("default"), m_map_sym("map"), m_set_union_sym("union"), - m_set_intersect_sym("intersect"), - m_set_difference_sym("difference"), + m_set_intersect_sym("intersection"), + m_set_difference_sym("setminus"), m_set_complement_sym("complement"), m_set_subset_sym("subset"), m_array_ext_sym("array-ext"), @@ -581,8 +581,8 @@ void array_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("map",OP_ARRAY_MAP)); op_names.push_back(builtin_name("default",OP_ARRAY_DEFAULT)); op_names.push_back(builtin_name("union",OP_SET_UNION)); - op_names.push_back(builtin_name("intersect",OP_SET_INTERSECT)); - op_names.push_back(builtin_name("difference",OP_SET_DIFFERENCE)); + op_names.push_back(builtin_name("intersection",OP_SET_INTERSECT)); + op_names.push_back(builtin_name("setminus",OP_SET_DIFFERENCE)); op_names.push_back(builtin_name("complement",OP_SET_COMPLEMENT)); op_names.push_back(builtin_name("subset",OP_SET_SUBSET)); op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); @@ -616,6 +616,13 @@ func_decl * array_recognizers::get_as_array_func_decl(expr * n) const { return to_func_decl(to_app(n)->get_decl()->get_parameter(0).get_ast()); } +func_decl * array_recognizers::get_map_func_decl(func_decl* f) const { + SASSERT(f->get_num_parameters() == 1); + SASSERT(f->get_parameter(0).is_ast()); + SASSERT(is_func_decl(f->get_parameter(0).get_ast())); + return to_func_decl(f->get_parameter(0).get_ast()); +} + func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const { SASSERT(is_as_array(f)); return to_func_decl(f->get_parameter(0).get_ast()); diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index e4725901e..130184a6e 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -164,6 +164,8 @@ public: 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; + func_decl * get_map_func_decl(func_decl* f) const; + func_decl * get_map_func_decl(expr* e) const { return get_map_func_decl(to_app(e)->get_decl()); } bool is_const(expr* e, expr*& v) const; @@ -190,6 +192,16 @@ public: parameter p(f); return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args); } + + expr * mk_map_assoc(func_decl * f, unsigned num_args, expr * const * args) { + expr* r = args[0]; + for (unsigned i = 1; i < num_args; ++i) { + expr* es[2] = { r, args[i] }; + r = mk_map(f, 2, es); + } + return r; + } + app * mk_const_array(sort * s, expr * v) { parameter param(s); return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, &v); @@ -201,6 +213,18 @@ public: return mk_const_array(s, m_manager.mk_true()); } + app * mk_setminus(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_DIFFERENCE, s1, s2); + } + + app * mk_intersection(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_INTERSECT, s1, s2); + } + + app * mk_union(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_SET_UNION, s1, s2); + } + app* mk_has_size(expr* set, expr* n) { return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 48daf6988..e9b6a9766 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -924,11 +924,11 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { decl_collector decls(m); smt_renaming rn; - for (unsigned i = 0; i < m_assumptions.size(); ++i) { - decls.visit(m_assumptions[i].get()); + for (expr* a : m_assumptions) { + decls.visit(a); } - for (unsigned i = 0; i < m_assumptions_star.size(); ++i) { - decls.visit(m_assumptions_star[i].get()); + for (expr* a : m_assumptions_star) { + decls.visit(a); } decls.visit(n); @@ -959,8 +959,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) { #else decls.order_deps(); ast_mark sort_mark; - for (unsigned i = 0; i < decls.get_num_sorts(); ++i) { - sort* s = decls.get_sorts()[i]; + for (sort* s : decls.get_sorts()) { if (!(*m_is_declared)(s)) { smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0); p.pp_sort_decl(sort_mark, s); diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 8945c0bec..a567f759c 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -57,8 +57,8 @@ public: unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); } - sort * const * get_sorts() const { return m_sorts.c_ptr(); } - func_decl * const * get_func_decls() const { return m_decls.c_ptr(); } + ptr_vector const& get_sorts() const { return m_sorts; } + ptr_vector const& get_func_decls() const { return m_decls; } }; #endif diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 3aef589b6..3fc413d67 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -45,10 +45,7 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c st = mk_store_core(num_args, args, result); break; case OP_ARRAY_MAP: - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_ast()); - SASSERT(is_func_decl(f->get_parameter(0).get_ast())); - st = mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result); + st = mk_map_core(m_util.get_map_func_decl(f), num_args, args, result); break; case OP_SET_UNION: st = mk_set_union(num_args, args, result); @@ -242,6 +239,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, return BR_FAILED; } +sort_ref array_rewriter::get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args) { + sort* s0 = m().get_sort(args[0]); + unsigned sz = get_array_arity(s0); + ptr_vector domain; + for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); + return sort_ref(m_util.mk_array_sort(sz, domain.c_ptr(), f->get_range()), m()); +} + br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { app* store_expr = nullptr; @@ -292,11 +297,7 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c } else { expr_ref value(m().mk_app(f, values.size(), values.c_ptr()), m()); - sort* s0 = m().get_sort(args[0]); - unsigned sz = get_array_arity(s0); - ptr_vector domain; - for (unsigned i = 0; i < sz; ++i) domain.push_back(get_array_domain(s0, i)); - sort_ref s(m_util.mk_array_sort(sz, domain.c_ptr(), m().get_sort(value)), m()); + sort_ref s = get_map_array_sort(f, num_args, args); result = m_util.mk_const_array(s, value); } return BR_REWRITE2; @@ -337,6 +338,75 @@ br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * c return BR_REWRITE3; } + if (m().is_and(f)) { + ast_mark mark; + ptr_buffer es; + bool change = false; + unsigned j = 0; + es.append(num_args, args); + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (mark.is_marked(e)) { + change = true; + } + else if (m_util.is_map(e) && m().is_and(m_util.get_map_func_decl(e))) { + mark.mark(e, true); + es.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + mark.mark(e, true); + es[j++] = es[i]; + } + } + es.shrink(j); + for (expr* e : es) { + if (m().is_not(e, e) && mark.is_marked(e)) { + sort_ref s = get_map_array_sort(f, num_args, args); + result = m_util.mk_const_array(s, m().mk_false()); + return BR_DONE; + } + } + if (change) { + result = m_util.mk_map_assoc(f, es.size(), es.c_ptr()); + return BR_DONE; + } + } + + if (m().is_or(f)) { + ast_mark mark; + ptr_buffer es; + es.append(num_args, args); + unsigned j = 0; + bool change = false; + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (mark.is_marked(e)) { + change = true; + } + else if (m_util.is_map(e) && m().is_or(m_util.get_map_func_decl(e))) { + mark.mark(e, true); + es.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + mark.mark(e, true); + es[j++] = es[i]; + } + } + es.shrink(j); + for (expr* e : es) { + if (m().is_not(e, e) && mark.is_marked(e)) { + sort_ref s = get_map_array_sort(f, num_args, args); + result = m_util.mk_const_array(s, m().mk_true()); + return BR_DONE; + } + } + if (change) { + result = m_util.mk_map_assoc(f, es.size(), es.c_ptr()); + return BR_DONE; + } + } + + return BR_FAILED; } diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index 056ef66c4..18fb74adb 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -37,6 +37,9 @@ class array_rewriter { lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2); bool has_index_set(expr* e, expr_ref& e0, vector& indices); void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls); + + sort_ref get_map_array_sort(func_decl* f, unsigned num_args, expr* const* args); + public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 9fbeced71..50d87029e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2033,10 +2033,8 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr // TODO: display uninterpreted sort decls, and datatype decls. - unsigned num_decls = decls.get_num_decls(); - func_decl * const * fs = decls.get_func_decls(); - for (unsigned i = 0; i < num_decls; i++) { - display(out, fs[i]); + for (func_decl* f : decls.get_func_decls()) { + display(out, f); out << std::endl; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 47a57c6d0..872b8c3e7 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -102,7 +102,7 @@ namespace smt { theory_array_full& th; arith_util m_arith; array_util m_autil; - array_rewriter m_rw; + th_rewriter m_rw; arith_value m_arith_value; ast_ref_vector m_pinned; obj_map m_sizeof; @@ -211,6 +211,9 @@ namespace smt { SASSERT(i2.m_is_leaf); expr* s = sz1->get_arg(0); expr* t = sz2->get_arg(0); + if (m.get_sort(s) != m.get_sort(t)) { + return true; + } enode* r1 = get_root(s); enode* r2 = get_root(t); if (r1 == r2) { @@ -265,11 +268,15 @@ namespace smt { } expr_ref mk_subtract(expr* t, expr* s) { - return m_rw.mk_set_difference(t, s); + expr_ref d(m_autil.mk_setminus(t, s), m); + m_rw(d); + return d; } expr_ref mk_intersect(expr* t, expr* s) { - return m_rw.mk_set_intersect(t, s); + expr_ref i(m_autil.mk_intersection(t, s), m); + m_rw(i); + return i; } void propagate(expr* assumption, expr* conseq) { diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 98f6be343..00ea59869 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -917,7 +917,7 @@ public: { // Warning: scoped_timer is not thread safe in Linux. scoped_timer timer(m_timeout, &eh); - m_t->operator()(in, result); + m_t->operator()(in, result); } }