add card operator to bapa

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<builtin_name>& 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: 
+    if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
-    // sort_names.push_back(builtin_name("Set", _SET_SORT));
+        // 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<builtin_name>& op_names, symbol const & logic) {
@@ -568,6 +588,7 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& 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));
     }
 }
 

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;

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";
+    CTRACE("array_rewriter", st != BR_FAILED, 
-          for (unsigned i = 0; i < num_args; ++i) {
+           tout << mk_pp(f, m()) << "\n";
-              tout << mk_pp(args[i], m()) << "\n";
+           for (unsigned i = 0; i < num_args; ++i) {
-          }
+               tout << mk_pp(args[i], m()) << "\n";
-          tout << "\n --> " << result << "\n";
+           }
-          );
+           tout << "\n --> " << result << "\n";);
     return st;
 }
 

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<enode, expr*> const& s, obj_map<enode, expr*> 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(); }
 

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();
     };

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);

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);