mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
expose cardinality declarations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f7cc68aa6a
commit
1203af83eb
|
@ -1051,6 +1051,8 @@ extern "C" {
|
|||
case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
|
||||
case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
|
||||
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:
|
||||
return Z3_OP_INTERNAL;
|
||||
}
|
||||
|
|
|
@ -1051,6 +1051,8 @@ typedef enum {
|
|||
Z3_OP_SET_SUBSET,
|
||||
Z3_OP_AS_ARRAY,
|
||||
Z3_OP_ARRAY_EXT,
|
||||
Z3_OP_SET_HAS_SIZE,
|
||||
Z3_OP_SET_CARD,
|
||||
|
||||
// Bit-vectors
|
||||
Z3_OP_BNUM = 0x400,
|
||||
|
|
Loading…
Reference in a new issue