add set-has-size to API and python bindings

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

src/api/api_array.cpp

@@ -263,6 +263,7 @@ extern "C" {
     MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
     MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
     MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
+    MK_BINARY(Z3_mk_set_has_size, mk_c(c)->get_array_fid(), OP_SET_HAS_SIZE, SKIP);
 
     Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
         Z3_TRY;

src/api/python/z3/z3.py

@@ -4504,6 +4504,11 @@ def Ext(a, b):
         _z3_assert(is_array(a) and is_array(b), "arguments must be arrays")
     return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
 
+def SetHasSize(a, k):
+    ctx = a.ctx
+    k = _py2expr(k, ctx)
+    return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
+
 def is_select(a):
     """Return `True` if `a` is a Z3 array select application.
 

src/api/z3_api.h

@@ -3106,6 +3106,14 @@ extern "C" {
        def_API('Z3_mk_as_array', AST, (_in(CONTEXT), _in(FUNC_DECL)))
      */
     Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
+
+    /**
+       \brief Create predicate that holds if Boolean array \c set has \c k elements set to true.       
+
+       def_API('Z3_mk_set_has_size', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
+
     /*@}*/
 
     /** @name Sets */

src/smt/theory_array_base.cpp

@@ -621,7 +621,7 @@ namespace smt {
             if (!ctx.is_relevant(n))
                 continue;
             
-            if (is_store(n) || is_const(n) || is_default(n))
+            if (is_store(n) || is_const(n) || is_default(n) || is_set_has_size(n))
                 return false;
         }
         return true;