diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 70cd5e66f..88c04129f 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -26,6 +26,19 @@ Revision History: finite_set_decl_plugin::finite_set_decl_plugin(): m_init(false) { + m_names.resize(LAST_FINITE_SET_OP, nullptr); + m_names[OP_FINITE_SET_EMPTY] = "set.empty "; + m_names[OP_FINITE_SET_SINGLETON] = "set.singleton"; + m_names[OP_FINITE_SET_UNION] = "set.union"; + m_names[OP_FINITE_SET_INTERSECT] = "set.intersect"; + m_names[OP_FINITE_SET_DIFFERENCE] = "set.difference"; + m_names[OP_FINITE_SET_IN] = "set.in"; + m_names[OP_FINITE_SET_SIZE] = "set.size"; + m_names[OP_FINITE_SET_SUBSET] = "set.subset"; + m_names[OP_FINITE_SET_MAP] = "set.map"; + m_names[OP_FINITE_SET_FILTER] = "set.filter"; + m_names[OP_FINITE_SET_RANGE] = "set.range"; + m_names[OP_FINITE_SET_EXT] = "set.diff"; } finite_set_decl_plugin::~finite_set_decl_plugin() { @@ -59,18 +72,18 @@ void finite_set_decl_plugin::init() { sort* intintT[2] = { intT, intT }; m_sigs.resize(LAST_FINITE_SET_OP); - m_sigs[OP_FINITE_SET_EMPTY] = alloc(polymorphism::psig, m, "set.empty", 1, 0, nullptr, setA); - m_sigs[OP_FINITE_SET_SINGLETON] = alloc(polymorphism::psig, m, "set.singleton", 1, 1, &A, setA); - m_sigs[OP_FINITE_SET_UNION] = alloc(polymorphism::psig, m, "set.union", 1, 2, setAsetA, setA); - m_sigs[OP_FINITE_SET_INTERSECT] = alloc(polymorphism::psig, m, "set.intersect", 1, 2, setAsetA, setA); - m_sigs[OP_FINITE_SET_DIFFERENCE] = alloc(polymorphism::psig, m, "set.difference", 1, 2, setAsetA, setA); - m_sigs[OP_FINITE_SET_IN] = alloc(polymorphism::psig, m, "set.in", 1, 2, AsetA, boolT); - m_sigs[OP_FINITE_SET_SIZE] = alloc(polymorphism::psig, m, "set.size", 1, 1, &setA, intT); - m_sigs[OP_FINITE_SET_SUBSET] = alloc(polymorphism::psig, m, "set.subset", 1, 2, setAsetA, boolT); - m_sigs[OP_FINITE_SET_MAP] = alloc(polymorphism::psig, m, "set.map", 2, 2, arrABsetA, setB); - m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, "set.filter", 1, 2, arrABoolsetA, setA); - m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, "set.range", 0, 2, intintT, setInt); - m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A); + m_sigs[OP_FINITE_SET_EMPTY] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EMPTY], 1, 0, nullptr, setA); + m_sigs[OP_FINITE_SET_SINGLETON] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_SINGLETON], 1, 1, &A, setA); + m_sigs[OP_FINITE_SET_UNION] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_UNION], 1, 2, setAsetA, setA); + m_sigs[OP_FINITE_SET_INTERSECT] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_INTERSECT], 1, 2, setAsetA, setA); + m_sigs[OP_FINITE_SET_DIFFERENCE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_DIFFERENCE], 1, 2, setAsetA, setA); + m_sigs[OP_FINITE_SET_IN] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_IN], 1, 2, AsetA, boolT); + m_sigs[OP_FINITE_SET_SIZE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_SIZE], 1, 1, &setA, intT); + m_sigs[OP_FINITE_SET_SUBSET] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_SUBSET], 1, 2, setAsetA, boolT); + m_sigs[OP_FINITE_SET_MAP] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_MAP], 2, 2, arrABsetA, setB); + m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_FILTER], 1, 2, arrABoolsetA, setA); + m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_RANGE], 0, 2, intintT, setInt); + m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EXT], 1, 2, setAsetA, A); // m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A); } @@ -187,11 +200,9 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param } void finite_set_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { - init(); - for (unsigned i = 0; i < m_sigs.size(); ++i) { - if (m_sigs[i]) - op_names.push_back(builtin_name(m_sigs[i]->m_name.str(), i)); - } + for (unsigned i = 0; i < m_names.size(); ++i) + if (m_names[i]) + op_names.push_back(builtin_name(std::string(m_names[i]), i)); } void finite_set_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { @@ -282,8 +293,10 @@ bool finite_set_decl_plugin::is_value(app * e) const { bool finite_set_decl_plugin::is_unique_value(app* e) const { // Empty set is a value + // A singleton of a unique value is tagged as unique + // ranges are not considered unique even if the bounds are values return is_app_of(e, m_family_id, OP_FINITE_SET_EMPTY) || - (is_app_of(e, m_family_id, OP_FINITE_SET_SINGLETON) && is_unique_value(to_app(e->get_arg(0)))); + (is_app_of(e, m_family_id, OP_FINITE_SET_SINGLETON) && m_manager->is_unique_value(to_app(e->get_arg(0)))); } bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const { @@ -294,8 +307,9 @@ bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const { return true; if (r.is_singleton(e1) && r.is_empty(e2)) return true; - if(r.is_singleton(e1) && r.is_singleton(e2)) - return m_manager->are_distinct(e1, e2); + expr *x = nullptr, *y = nullptr; + if(r.is_singleton(e1, x) && r.is_singleton(e2, y)) + return m_manager->are_distinct(x, y); // TODO: could be extended to cases where we can prove the sets are different by containing one element // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b. diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 6756b140a..9084648b6 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -54,7 +54,8 @@ enum finite_set_op_kind { class finite_set_decl_plugin : public decl_plugin { ptr_vector m_sigs; - bool m_init; + svector m_names; + bool m_init = false; void init(); func_decl * mk_empty(sort* set_sort); diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp index 3ce28557d..9e2aaa3a6 100644 --- a/src/ast/rewriter/finite_set_rewriter.cpp +++ b/src/ast/rewriter/finite_set_rewriter.cpp @@ -17,6 +17,7 @@ Author: #include "ast/rewriter/finite_set_rewriter.h" #include "ast/arith_decl_plugin.h" +#include "ast/ast_pp.h" br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_family_id() == get_fid()); @@ -39,7 +40,6 @@ br_status finite_set_rewriter::mk_app_core(func_decl * f, unsigned num_args, exp SASSERT(num_args == 2); return mk_in(args[0], args[1], result); case OP_FINITE_SET_SIZE: - // Size is already in normal form, no simplifications return mk_size(args[0], result); default: return BR_FAILED; @@ -55,18 +55,18 @@ br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args, // Identity: set.union(x, empty) -> x or set.union(empty, x) -> x if (num_args == 2) { - if (m_util.is_empty(args[0])) { + if (u.is_empty(args[0])) { result = args[1]; return BR_DONE; } - if (m_util.is_empty(args[1])) { + if (u.is_empty(args[1])) { result = args[0]; return BR_DONE; } // Absorption: set.union(x, set.intersect(x, y)) -> x expr* a1, *a2; - if (m_util.is_intersect(args[1], a1, a2)) { + if (u.is_intersect(args[1], a1, a2)) { if (args[0] == a1 || args[0] == a2) { result = args[0]; return BR_DONE; @@ -74,7 +74,7 @@ br_status finite_set_rewriter::mk_union(unsigned num_args, expr * const * args, } // Absorption: set.union(set.intersect(x, y), x) -> x - if (m_util.is_intersect(args[0], a1, a2)) { + if (u.is_intersect(args[0], a1, a2)) { if (args[1] == a1 || args[1] == a2) { result = args[1]; return BR_DONE; @@ -94,18 +94,18 @@ br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * ar // Annihilation: set.intersect(x, empty) -> empty or set.intersect(empty, x) -> empty if (num_args == 2) { - if (m_util.is_empty(args[0])) { + if (u.is_empty(args[0])) { result = args[0]; return BR_DONE; } - if (m_util.is_empty(args[1])) { + if (u.is_empty(args[1])) { result = args[1]; return BR_DONE; } // Absorption: set.intersect(x, set.union(x, y)) -> x expr* a1, *a2; - if (m_util.is_union(args[1], a1, a2)) { + if (u.is_union(args[1], a1, a2)) { if (args[0] == a1 || args[0] == a2) { result = args[0]; return BR_DONE; @@ -113,7 +113,7 @@ br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * ar } // Absorption: set.intersect(set.union(x, y), x) -> x - if (m_util.is_union(args[0], a1, a2)) { + if (u.is_union(args[0], a1, a2)) { if (args[1] == a1 || args[1] == a2) { result = args[1]; return BR_DONE; @@ -128,19 +128,19 @@ br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref // set.difference(x, x) -> set.empty if (arg1 == arg2) { sort* set_sort = arg1->get_sort(); - SASSERT(m_util.is_finite_set(set_sort)); - result = m_util.mk_empty(set_sort); + SASSERT(u.is_finite_set(set_sort)); + result = u.mk_empty(set_sort); return BR_DONE; } // Identity: set.difference(x, empty) -> x - if (m_util.is_empty(arg2)) { + if (u.is_empty(arg2)) { result = arg1; return BR_DONE; } // Annihilation: set.difference(empty, x) -> empty - if (m_util.is_empty(arg1)) { + if (u.is_empty(arg1)) { result = arg1; return BR_DONE; } @@ -156,20 +156,20 @@ br_status finite_set_rewriter::mk_subset(expr * arg1, expr * arg2, expr_ref & re } // set.subset(empty, x) -> true - if (m_util.is_empty(arg1)) { + if (u.is_empty(arg1)) { result = m.mk_true(); return BR_DONE; } // set.subset(x, empty) -> x = empty - if (m_util.is_empty(arg2)) { + if (u.is_empty(arg2)) { result = m.mk_eq(arg1, arg2); return BR_REWRITE1; } // General case: set.subset(x, y) -> set.intersect(x, y) = x expr_ref intersect(m); - intersect = m_util.mk_intersect(arg1, arg2); + intersect = u.mk_intersect(arg1, arg2); result = m.mk_eq(intersect, arg1); return BR_REWRITE3; } @@ -181,18 +181,18 @@ br_status finite_set_rewriter::mk_singleton(expr * arg, expr_ref & result) { br_status finite_set_rewriter::mk_size(expr * arg, expr_ref & result) { arith_util a(m); - if (m_util.is_empty(arg)) { + if (u.is_empty(arg)) { // size(empty) -> 0 result = a.mk_int(0); return BR_DONE; } - if (m_util.is_singleton(arg)) { + if (u.is_singleton(arg)) { // size(singleton(x)) -> 1 result = a.mk_int(1); return BR_DONE; } expr *lower, *upper; - if (m_util.is_range(arg, lower, upper)) { + if (u.is_range(arg, lower, upper)) { // size(range(a, b)) -> b - a + 1 expr_ref size_expr(m); size_expr = a.mk_add(a.mk_sub(upper, lower), a.mk_int(1)); @@ -205,14 +205,14 @@ br_status finite_set_rewriter::mk_size(expr * arg, expr_ref & result) { br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) { // set.in(x, empty) -> false - if (m_util.is_empty(set)) { + if (u.is_empty(set)) { result = m.mk_false(); return BR_DONE; } // set.in(x, singleton(y)) checks expr* singleton_elem; - if (m_util.is_singleton(set, singleton_elem)) { + if (u.is_singleton(set, singleton_elem)) { // set.in(x, singleton(x)) -> true (when x is the same) if (elem == singleton_elem) { result = m.mk_true(); @@ -222,6 +222,12 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) result = m.mk_eq(elem, singleton_elem); return BR_REWRITE1; } + expr *lo = nullptr, *hi = nullptr; + if (u.is_range(set, lo, hi)) { + arith_util a(m); + result = m.mk_and(a.mk_le(lo, elem), a.mk_le(elem, hi)); + return BR_REWRITE2; + } // NB we don't rewrite (set.in x (set.union s t)) to (or (set.in x s) (set.in x t)) // because it creates two new sub-expressions. The expression (set.union s t) could // be shared with other expressions so the net effect of this rewrite could be to create @@ -248,18 +254,169 @@ br_status finite_set_rewriter::mk_in(expr * elem, expr * set, expr_ref & result) * min({}) = {} * min([l..u]) = [l..u] u {} * min(s u t) = -* let range_s u s1 = min(s) -* let range_t u t1 = min(t) -* if range_s < range_t: -* range_s u (t u s1) -* if range_t < range_t: -* range_t u (s u t1) -* if range_t n range_s != {}: -* min(range_t, range_s) u the rest ... -* etc. +* let {x} u s1 = min(s) +* let {y} u t1 = min(t) +* if x = y then +* { x } u (s1 u t1) +* else if x < y then +* {x} u (s1 u ({y} u t1) +* else // x > y +* {y} u (t1 u ({x} u s1) +* +* Handling ranges is TBD +* For proper range handling we have to change is_less on numeric singleton sets +* to use the numerical value, not the expression identifier. Then the ordering +* has to make all numeric values less than symbolic values. */ -br_status finite_set_rewriter::mk_eq_core(expr* a, expr* b, expr_ref& result) { +bool finite_set_rewriter::is_less(expr *a, expr *b) { + return a->get_id() < b->get_id(); +} - return BR_FAILED; -} \ No newline at end of file +expr* finite_set_rewriter::mk_union(expr* a, expr* b) { + if (u.is_empty(a)) + return b; + if (u.is_empty(b)) + return a; + if (a == b) + return a; + return u.mk_union(a, b); +} + +expr* finite_set_rewriter::min(expr* e) { + if (m_is_min.is_marked(e)) + return e; + expr *a = nullptr, *b = nullptr; + if (u.is_union(e, a, b)) { + a = min(a); + b = min(b); + if (u.is_empty(a)) + return b; + if (u.is_empty(b)) + return a; + auto [x,a1] = get_min(a); + auto [y,b1] = get_min(b); + if (x == y) + a = mk_union(x, mk_union(a1, b1)); + else if (is_less(x, y)) + a = mk_union(x, mk_union(a1, b)); + else + a = mk_union(y, mk_union(a, b1)); + m_pinned.push_back(a); + m_is_min.mark(a); + return a; + } + if (u.is_intersect(e, a, b)) { + if (!from_unique_values(a) || !from_unique_values(b)) { + m_pinned.push_back(e); + m_is_min.mark(e); + return e; + } + while (true) { + a = min(a); + b = min(b); + if (u.is_empty(a)) + return a; + if (u.is_empty(b)) + return b; + auto [x, a1] = get_min(a); + auto [y, b1] = get_min(b); + if (x == y) { + a = mk_union(x, u.mk_intersect(a1, b1)); + m_pinned.push_back(a); + m_is_min.mark(a); + return a; + } + else if (is_less(x, y)) + a = a1; + else + b = b1; + } + } + if (u.is_difference(e, a, b)) { + if (!from_unique_values(a) || !from_unique_values(b)) { + m_pinned.push_back(e); + m_is_min.mark(e); + return e; + } + while (true) { + a = min(a); + b = min(b); + if (u.is_empty(a) || u.is_empty(b)) + return a; + auto [x, a1] = get_min(a); + auto [y, b1] = get_min(b); + if (x == y) { + a = a1; + b = b1; + } + else if (is_less(x, y)) { + a = mk_union(x, u.mk_difference(a1, b)); + m_pinned.push_back(a); + m_is_min.mark(a); + return a; + } + else { + b = b1; + } + } + } + // set.filter, set.map don't have decompositions + m_pinned.push_back(e); + m_is_min.mark(e); + return e; +} + +std::pair finite_set_rewriter::get_min(expr* a) { + expr *x = nullptr, *y = nullptr; + if (u.is_union(a, x, y)) + return {x, y}; + auto empty = u.mk_empty(a->get_sort()); + m_pinned.push_back(empty); + return {a, empty}; +} + +br_status finite_set_rewriter::mk_eq_core(expr *a, expr *b, expr_ref &result) { + m_is_min.reset(); + m_pinned.reset(); + bool are_unique = true; + while (true) { + if (a == b) { + result = m.mk_true(); + return BR_DONE; + } + TRACE(finite_set, tout << mk_pp(a, m) << " == " << mk_pp(b, m) << "\n"); + a = min(a); + b = min(b); + auto [x, a1] = get_min(a); + auto [y, b1] = get_min(b); + + // only empty sets and singletons of unique values are unique. + // ranges are not counted as unique. + are_unique &= m.is_unique_value(x) && m.is_unique_value(y); + a = a1; + b = b1; + if (x == y) + continue; + + if (m.are_distinct(x, y) && are_unique) { + are_unique &= from_unique_values(a); + are_unique &= from_unique_values(b); + if (are_unique) { + result = m.mk_false(); + return BR_DONE; + } + } + return BR_FAILED; + } +} + +bool finite_set_rewriter::from_unique_values(expr *a) { + while (!u.is_empty(a)) { + auto [x, a1] = get_min(min(a)); + if (!m.is_unique_value(x)) + return false; + a = a1; + } + return true; +} diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h index 21e2158c7..062bf9a08 100644 --- a/src/ast/rewriter/finite_set_rewriter.h +++ b/src/ast/rewriter/finite_set_rewriter.h @@ -35,7 +35,15 @@ where the signature is defined in finite_set_decl_plugin.h. class finite_set_rewriter { friend class finite_set_rewriter_test; ast_manager &m; - finite_set_util m_util; + finite_set_util u; + expr_ref_vector m_pinned; + expr_mark m_is_min; + + expr * min(expr *a); + std::pair get_min(expr *a); + bool is_less(expr *a, expr *b); + expr *mk_union(expr *a, expr *b); + bool from_unique_values(expr *a); // Rewrite rules for set operations br_status mk_union(unsigned num_args, expr *const *args, expr_ref &result); @@ -48,11 +56,11 @@ class finite_set_rewriter { public: finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m(m), m_util(m) { + m(m), u(m), m_pinned(m) { } - family_id get_fid() const { return m_util.get_family_id(); } - finite_set_util& util() { return m_util; } + family_id get_fid() const { return u.get_family_id(); } + finite_set_util& util() { return u; } br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d541781ea..aa8fb0897 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -335,6 +335,7 @@ namespace smt { for (unsigned i = 0; i < num_args; i++) { enode * arg = e->get_arg(i); sort * s = arg->get_sort(); + sort *e_sort = nullptr; if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) { app_ref def(m_autil.mk_default(arg->get_expr()), m); if (!ctx.e_internalized(def)) { @@ -342,6 +343,13 @@ namespace smt { } arg = ctx.get_enode(def); } + if (m_fsutil.is_finite_set(s, e_sort) && m_util.is_datatype(e_sort)) { + app_ref def(m_fsutil.mk_empty(s), m); + if (!ctx.e_internalized(def)) { + ctx.internalize(def, false); + } + arg = ctx.get_enode(def); + } if (!m_util.is_datatype(s) && !m_sutil.is_seq(s)) continue; if (is_attached_to_var(arg)) @@ -532,8 +540,9 @@ namespace smt { found = true; } sort * s = arg->get_sort(); - if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) { - for (enode* aarg : get_array_args(arg)) { + sort *se = nullptr; + auto add_args = [&](ptr_vector const &args) { + for (enode *aarg : args) { if (aarg->get_root() == child->get_root()) { if (aarg != child) { m_used_eqs.push_back(enode_pair(aarg, child)); @@ -541,17 +550,16 @@ namespace smt { found = true; } } + }; + if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) { + add_args(get_array_args(arg)); + } + if (m_fsutil.is_finite_set(s, se) && m_util.is_datatype(se)) { + add_args(get_finite_set_args(arg)); } - sort* se = nullptr; if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) { - enode* sibling; - for (enode* aarg : get_seq_args(arg, sibling)) { - if (aarg->get_root() == child->get_root()) { - if (aarg != child) - m_used_eqs.push_back(enode_pair(aarg, child)); - found = true; - } - } + enode *sibling = nullptr; + add_args(get_seq_args(arg, sibling)); if (sibling && sibling != arg) m_used_eqs.push_back(enode_pair(arg, sibling)); @@ -640,6 +648,11 @@ namespace smt { return true; } } + else if (m_fsutil.is_finite_set(s, se) && m_util.is_datatype(se)) { + for (enode *aarg : get_finite_set_args(arg)) + if (process_arg(aarg)) + return true; + } else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) { for (enode* aarg : get_array_args(arg)) if (process_arg(aarg)) @@ -649,6 +662,33 @@ namespace smt { return false; } + ptr_vector const &theory_datatype::get_finite_set_args(enode *n) { + m_args.reset(); + m_todo.reset(); + auto add_todo = [&](enode *n) { + if (!n->is_marked()) { + n->set_mark(); + m_todo.push_back(n); + } + }; + add_todo(n); + + for (unsigned i = 0; i < m_todo.size(); ++i) { + enode *n = m_todo[i]; + expr *e = n->get_expr(); + if (m_fsutil.is_singleton(e)) + m_args.push_back(n->get_arg(0)); + else if (m_fsutil.is_union(e)) + for (auto k : enode::args(n)) + add_todo(k); + } + for (enode *n : m_todo) + n->unset_mark(); + + return m_args; + } + + ptr_vector const& theory_datatype::get_seq_args(enode* n, enode*& sibling) { m_args.reset(); m_todo.reset(); @@ -762,6 +802,7 @@ namespace smt { m_util(m), m_autil(m), m_sutil(m), + m_fsutil(m), m_find(*this) { } diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 8a61ce5bd..12bd9ae9c 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -21,6 +21,7 @@ Revision History: #include "util/union_find.h" #include "ast/array_decl_plugin.h" #include "ast/seq_decl_plugin.h" +#include "ast/finite_set_decl_plugin.h" #include "ast/datatype_decl_plugin.h" #include "model/datatype_factory.h" #include "smt/smt_theory.h" @@ -48,6 +49,7 @@ namespace smt { datatype_util m_util; array_util m_autil; seq_util m_sutil; + finite_set_util m_fsutil; ptr_vector m_var_data; th_union_find m_find; trail_stack m_trail_stack; @@ -95,6 +97,7 @@ namespace smt { ptr_vector m_args, m_todo; ptr_vector const& get_array_args(enode* n); ptr_vector const& get_seq_args(enode* n, enode*& sibling); + ptr_vector const& get_finite_set_args(enode *n); // class for managing state of final_check class final_check_st { diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index ef281097a..a234acdfd 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -690,6 +690,7 @@ namespace smt { continue; out << "watch[" << i << "] := " << m_clauses.watch[i] << "\n"; } + m_cardinality_solver.display(out); } void theory_finite_set::init_model(model_generator & mg) { diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index e3b8dd651..c35a6d6a8 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -65,7 +65,7 @@ namespace smt { expr_ref_vector bs(m); for (auto n : ns) { std::ostringstream strm; - strm << enode_pp(n, ctx); + strm << "|" << enode_pp(n, ctx) << "|"; symbol name = symbol(strm.str()); expr_ref b(m.mk_const(name, m.mk_bool_sort()), m); bs.push_back(b); @@ -401,7 +401,7 @@ namespace smt { return false; } - std::ostream& theory_finite_set_size::display(std::ostream& out) { + std::ostream& theory_finite_set_size::display(std::ostream& out) const { if (m_solver) m_solver->display(out); return out; diff --git a/src/smt/theory_finite_set_size.h b/src/smt/theory_finite_set_size.h index bffd55598..182912861 100644 --- a/src/smt/theory_finite_set_size.h +++ b/src/smt/theory_finite_set_size.h @@ -68,6 +68,6 @@ namespace smt { void add_theory_assumptions(expr_ref_vector &assumptions); bool should_research(expr_ref_vector &unsat_core); lbool final_check(); - std::ostream &display(std::ostream &out); + std::ostream &display(std::ostream &out) const; }; } \ No newline at end of file