From 1203af83eb5c8c106e9ce7799b889f8961f9eba0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 24 Sep 2019 12:29:19 -0700 Subject: [PATCH] expose cardinality declarations Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 2 ++ src/api/z3_api.h | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 604e00f7f..5def91086 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -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; } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 974f71ea8..6909bb33d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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,