From 7e2afca2c60b4418f11a42bc7cb9762819d07623 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2019 13:24:07 -0700 Subject: [PATCH] add card operator to bapa Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 27 +++++++++++++++++++++--- src/ast/array_decl_plugin.h | 6 ++++++ src/ast/rewriter/array_rewriter.cpp | 15 +++++++------- src/smt/theory_array_bapa.cpp | 32 +++++++++++++++++++++++------ src/smt/theory_array_bapa.h | 2 +- src/smt/theory_array_base.h | 2 ++ src/smt/theory_array_full.cpp | 6 +++--- 7 files changed, 70 insertions(+), 20 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index f7a299131..071a35af0 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -36,7 +36,8 @@ array_decl_plugin::array_decl_plugin(): m_set_subset_sym("subset"), m_array_ext_sym("array-ext"), m_as_array_sym("as-array"), - m_set_has_size_sym("set-has-size") { + m_set_has_size_sym("set-has-size"), + m_set_card_sym("card") { } #define ARRAY_SORT_STR "Array" @@ -440,6 +441,21 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma func_decl_info(m_family_id, OP_SET_SUBSET)); } +func_decl * array_decl_plugin::mk_set_card(unsigned arity, sort * const* domain) { + if (arity != 1) { + m_manager->raise_exception("card takes only one argument"); + return nullptr; + } + + arith_util arith(*m_manager); + if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) { + m_manager->raise_exception("card expects an array of Booleans"); + } + sort * int_sort = arith.mk_int(); + return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort, + func_decl_info(m_family_id, OP_SET_CARD)); +} + func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) { if (arity != 2) { m_manager->raise_exception("set-has-size takes two arguments"); @@ -525,6 +541,8 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_set_subset(arity, domain); case OP_SET_HAS_SIZE: return mk_set_has_size(arity, domain); + case OP_SET_CARD: + return mk_set_card(arity, domain); case OP_AS_ARRAY: { if (num_parameters != 1 || !parameters[0].is_ast() || @@ -548,8 +566,10 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters void array_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT)); sort_names.push_back(builtin_name("=>", ARRAY_SORT)); - // TBD: this could easily break users even though it is already used in CVC4: - // sort_names.push_back(builtin_name("Set", _SET_SORT)); + if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) { + // this could easily break users even though it is already used in CVC4: + sort_names.push_back(builtin_name("Set", _SET_SORT)); + } } void array_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { @@ -568,6 +588,7 @@ void array_decl_plugin::get_op_names(svector& 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("set-has-size", OP_SET_HAS_SIZE)); + op_names.push_back(builtin_name("card", OP_SET_CARD)); } } diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index 6ba129444..e4725901e 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -52,6 +52,7 @@ enum array_op_kind { OP_SET_COMPLEMENT, OP_SET_SUBSET, OP_SET_HAS_SIZE, + OP_SET_CARD, OP_AS_ARRAY, // used for model construction LAST_ARRAY_OP }; @@ -70,6 +71,7 @@ class array_decl_plugin : public decl_plugin { symbol m_array_ext_sym; symbol m_as_array_sym; symbol m_set_has_size_sym; + symbol m_set_card_sym; bool check_set_arguments(unsigned arity, sort * const * domain); @@ -99,6 +101,8 @@ class array_decl_plugin : public decl_plugin { func_decl* mk_set_has_size(unsigned arity, sort * const* domain); + func_decl* mk_set_card(unsigned arity, sort * const* domain); + bool is_array_sort(sort* s) const; public: array_decl_plugin(); @@ -149,12 +153,14 @@ public: 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); } + 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); } 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_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_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; diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 61860ec4b..3aef589b6 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -69,14 +69,15 @@ br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c st = mk_set_difference(args[0], args[1], result); break; default: - return BR_FAILED; + st = BR_FAILED; + break; } - TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n"; - for (unsigned i = 0; i < num_args; ++i) { - tout << mk_pp(args[i], m()) << "\n"; - } - tout << "\n --> " << result << "\n"; - ); + CTRACE("array_rewriter", st != BR_FAILED, + tout << mk_pp(f, m()) << "\n"; + for (unsigned i = 0; i < num_args; ++i) { + tout << mk_pp(args[i], m()) << "\n"; + } + tout << "\n --> " << result << "\n";); return st; } diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 1dce9832d..47a57c6d0 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -204,7 +204,7 @@ namespace smt { return l_true; } - lbool ensure_disjoint(app* sz1, app* sz2) { + bool ensure_disjoint(app* sz1, app* sz2) { sz_info& i1 = *m_sizeof[sz1]; sz_info& i2 = *m_sizeof[sz2]; SASSERT(i1.m_is_leaf); @@ -214,16 +214,16 @@ namespace smt { enode* r1 = get_root(s); enode* r2 = get_root(t); if (r1 == r2) { - return l_true; + return true; } if (!ctx().is_diseq(r1, r2) && ctx().assume_eq(r1, r2)) { - return l_false; + return false; } if (do_intersect(i1.m_selects, i2.m_selects)) { add_disjoint(sz1, sz2); - return l_false; + return false; } - return l_true; + return true; } bool do_intersect(obj_map const& s, obj_map const& t) const { @@ -436,6 +436,15 @@ namespace smt { reset(); } + void internalize_term(app* term) { + if (th.is_set_has_size(term)) { + internalize_size(term); + } + else if (th.is_set_card(term)) { + internalize_card(term); + } + } + /** * Size(S, n) => n >= 0, default(S) = false */ @@ -458,6 +467,17 @@ namespace smt { ctx().push_trail(remove_sz(m_sizeof, term)); } + /** + \brief whenever there is a cardinality function, it includes an axiom + that entails the set is finite. + */ + void internalize_card(app* term) { + SASSERT(ctx().e_internalized(term)); + app_ref has_size(m_autil.mk_has_size(term->get_arg(0), term), m); + literal lit = mk_literal(has_size); + ctx().assign(lit, nullptr); + } + final_check_status final_check() { lbool r = ensure_functional(); if (r == l_true) update_indices(); @@ -494,7 +514,7 @@ namespace smt { theory_array_bapa::~theory_array_bapa() { dealloc(m_imp); } - void theory_array_bapa::internalize_size(app* term) { m_imp->internalize_size(term); } + void theory_array_bapa::internalize_term(app* term) { m_imp->internalize_term(term); } final_check_status theory_array_bapa::final_check() { return m_imp->final_check(); } diff --git a/src/smt/theory_array_bapa.h b/src/smt/theory_array_bapa.h index e99843cdd..5ac51f8a9 100644 --- a/src/smt/theory_array_bapa.h +++ b/src/smt/theory_array_bapa.h @@ -32,7 +32,7 @@ namespace smt { public: theory_array_bapa(theory_array_full& th); ~theory_array_bapa(); - void internalize_size(app* term); + void internalize_term(app* term); final_check_status final_check(); void init_model(); }; diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 5a6321379..3fc8be613 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -43,6 +43,7 @@ namespace smt { bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); } bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); } bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); } + bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); } bool is_store(enode const * n) const { return is_store(n->get_owner()); } bool is_map(enode const* n) const { return is_map(n->get_owner()); } @@ -52,6 +53,7 @@ namespace smt { bool is_default(enode const* n) const { return is_default(n->get_owner()); } bool is_array_sort(enode const* n) const { return is_array_sort(n->get_owner()); } bool is_set_has_size(enode const* n) const { return is_set_has_size(n->get_owner()); } + bool is_set_carde(enode const* n) const { return is_set_card(n->get_owner()); } app * mk_select(unsigned num_args, expr * const * args); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index 4457d99ff..ce8def177 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -250,7 +250,7 @@ namespace smt { return theory_array::internalize_term(n); } - if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n)) { + if (!is_const(n) && !is_default(n) && !is_map(n) && !is_as_array(n) && !is_set_has_size(n) && !is_set_card(n)) { if (!is_array_ext(n)) found_unsupported_op(n); return false; @@ -274,11 +274,11 @@ namespace smt { mk_var(arg0); } } - else if (is_set_has_size(n)) { + else if (is_set_has_size(n) || is_set_card(n)) { if (!m_bapa) { m_bapa = alloc(theory_array_bapa, *this); } - m_bapa->internalize_size(n); + m_bapa->internalize_term(n); } enode* node = ctx.get_enode(n);