mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

add parameter validation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-19 14:02:59 -08:00
parent ee03533c3a
commit 5bd7d93b55
1 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/api/api_finite_set.cpp
View file

@ -70,6 +70,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_singleton(c, elem);
RESET_ERROR_CODE();
CHECK_IS_EXPR(elem, nullptr);
app* a = mk_c(c)->fsutil().mk_singleton(to_expr(elem));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -80,6 +81,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_union(c, s1, s2);
RESET_ERROR_CODE();
CHECK_IS_EXPR(s1, nullptr);
CHECK_IS_EXPR(s2, nullptr);
app* a = mk_c(c)->fsutil().mk_union(to_expr(s1), to_expr(s2));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -90,6 +93,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_intersect(c, s1, s2);
RESET_ERROR_CODE();
CHECK_IS_EXPR(s1, nullptr);
CHECK_IS_EXPR(s2, nullptr);
app* a = mk_c(c)->fsutil().mk_intersect(to_expr(s1), to_expr(s2));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -100,6 +105,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_difference(c, s1, s2);
RESET_ERROR_CODE();
CHECK_IS_EXPR(s1, nullptr);
CHECK_IS_EXPR(s2, nullptr);
app* a = mk_c(c)->fsutil().mk_difference(to_expr(s1), to_expr(s2));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -110,6 +117,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_member(c, elem, set);
RESET_ERROR_CODE();
CHECK_IS_EXPR(elem, nullptr);
CHECK_IS_EXPR(set, nullptr);
app* a = mk_c(c)->fsutil().mk_in(to_expr(elem), to_expr(set));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -120,6 +129,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_size(c, set);
RESET_ERROR_CODE();
CHECK_IS_EXPR(set, nullptr);
app* a = mk_c(c)->fsutil().mk_size(to_expr(set));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -130,6 +140,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_subset(c, s1, s2);
RESET_ERROR_CODE();
CHECK_IS_EXPR(s1, nullptr);
CHECK_IS_EXPR(s2, nullptr);
app* a = mk_c(c)->fsutil().mk_subset(to_expr(s1), to_expr(s2));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -140,6 +152,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_map(c, f, set);
RESET_ERROR_CODE();
CHECK_IS_EXPR(f, nullptr);
CHECK_IS_EXPR(set, nullptr);
app* a = mk_c(c)->fsutil().mk_map(to_expr(f), to_expr(set));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -150,6 +164,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_filter(c, f, set);
RESET_ERROR_CODE();
CHECK_IS_EXPR(f, nullptr);
CHECK_IS_EXPR(set, nullptr);
app* a = mk_c(c)->fsutil().mk_filter(to_expr(f), to_expr(set));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -160,6 +176,8 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_finite_set_range(c, low, high);
RESET_ERROR_CODE();
CHECK_IS_EXPR(low, nullptr);
CHECK_IS_EXPR(high, nullptr);
app* a = mk_c(c)->fsutil().mk_range(to_expr(low), to_expr(high));
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));