mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-08 12:53:25 +00:00
Code Activity

remove references to set_has_size

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-11-26 13:57:24 -08:00
parent fab414a7ab
commit ed8b92411e
4 changed files with 1 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_array.cpp
View file

@ -268,7 +268,6 @@ extern "C" {
MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP); 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_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_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_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
Z3_TRY; Z3_TRY;

2
src/api/api_ast.cpp
View file

@ -1192,8 +1192,6 @@ extern "C" {
case OP_SET_SUBSET: return Z3_OP_SET_SUBSET; case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
case OP_AS_ARRAY: return Z3_OP_AS_ARRAY; case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT; case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
case OP_SET_CARD: return Z3_OP_SET_CARD;
case OP_SET_HAS_SIZE: return Z3_OP_SET_HAS_SIZE;
default: default:
return Z3_OP_INTERNAL; return Z3_OP_INTERNAL;
} }

9
src/api/python/z3/z3.py
View file

@ -5010,13 +5010,6 @@ def Ext(a, b):
_z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays") _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) 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): def is_select(a):
"""Return `True` if `a` is a Z3 array select application. """Return `True` if `a` is a Z3 array select application.
@ -10039,7 +10032,7 @@ class FPNumRef(FPRef):
""" """
def sign(self): def sign(self):
num = (ctypes.c_bool)() num = ctypes.c_bool()
nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num)) nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
if nsign is False: if nsign is False:
raise Z3Exception("error retrieving the sign of a numeral.") raise Z3Exception("error retrieving the sign of a numeral.")

8
src/api/z3_api.h
View file

@ -1037,8 +1037,6 @@ typedef enum {
Z3_OP_SET_SUBSET, Z3_OP_SET_SUBSET,
Z3_OP_AS_ARRAY, Z3_OP_AS_ARRAY,
Z3_OP_ARRAY_EXT, Z3_OP_ARRAY_EXT,
Z3_OP_SET_HAS_SIZE,
Z3_OP_SET_CARD,
// Bit-vectors // Bit-vectors
Z3_OP_BNUM = 0x400, Z3_OP_BNUM = 0x400,
@ -3316,12 +3314,6 @@ extern "C" {
*/ */
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f); 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);
/**@}*/ /**@}*/