Skip to content

Commit 934455a

Browse files
authored
Remove vestiges of old ml api (#7597)
1 parent e4897ff commit 934455a

File tree

3 files changed

+5
-10
lines changed

3 files changed

+5
-10
lines changed

examples/c/test_capi.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -592,7 +592,7 @@ void display_function_interpretations(Z3_context c, FILE * out, Z3_model m)
592592
Z3_symbol name;
593593
Z3_ast func_else;
594594
unsigned num_entries = 0, j;
595-
Z3_func_interp_opt finterp;
595+
Z3_func_interp finterp;
596596

597597
fdecl = Z3_model_get_func_decl(c, m, i);
598598
finterp = Z3_model_get_func_interp(c, m, fdecl);

src/api/api_model.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ extern "C" {
5959
Z3_CATCH;
6060
}
6161

62-
Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
62+
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
6363
Z3_TRY;
6464
LOG_Z3_model_get_const_interp(c, m, a);
6565
RESET_ERROR_CODE();

src/api/z3_api.h

+3-8
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,8 @@ DEFINE_TYPE(Z3_symbol);
88
DEFINE_TYPE(Z3_config);
99
DEFINE_TYPE(Z3_context);
1010
DEFINE_TYPE(Z3_sort);
11-
#define Z3_sort_opt Z3_sort
1211
DEFINE_TYPE(Z3_func_decl);
1312
DEFINE_TYPE(Z3_ast);
14-
#define Z3_ast_opt Z3_ast
1513
DEFINE_TYPE(Z3_app);
1614
DEFINE_TYPE(Z3_pattern);
1715
DEFINE_TYPE(Z3_model);
@@ -31,7 +29,6 @@ DEFINE_TYPE(Z3_ast_vector);
3129
DEFINE_TYPE(Z3_ast_map);
3230
DEFINE_TYPE(Z3_apply_result);
3331
DEFINE_TYPE(Z3_func_interp);
34-
#define Z3_func_interp_opt Z3_func_interp
3532
DEFINE_TYPE(Z3_func_entry);
3633
DEFINE_TYPE(Z3_fixedpoint);
3734
DEFINE_TYPE(Z3_optimize);
@@ -2083,7 +2080,7 @@ extern "C" {
20832080
Z3_symbol recognizer,
20842081
unsigned num_fields,
20852082
Z3_symbol const field_names[],
2086-
Z3_sort_opt const sorts[],
2083+
Z3_sort const sorts[],
20872084
unsigned sort_refs[]
20882085
);
20892086

@@ -5511,7 +5508,7 @@ extern "C" {
55115508
55125509
def_API('Z3_model_get_const_interp', AST, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
55135510
*/
5514-
Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
5511+
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a);
55155512

55165513
/**
55175514
\brief Test if there exists an interpretation (i.e., assignment) for \c a in the model \c m.
@@ -5532,7 +5529,7 @@ extern "C" {
55325529
55335530
def_API('Z3_model_get_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
55345531
*/
5535-
Z3_func_interp_opt Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
5532+
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f);
55365533

55375534
/**
55385535
\brief Return the number of constants assigned by the given model.
@@ -6033,7 +6030,6 @@ extern "C" {
60336030

60346031
/** @name Error Handling */
60356032
/**@{*/
6036-
#ifndef SAFE_ERRORS
60376033
/**
60386034
\brief Return the error code for the last API call.
60396035
@@ -6059,7 +6055,6 @@ extern "C" {
60596055
\sa Z3_get_error_code
60606056
*/
60616057
void Z3_API Z3_set_error_handler(Z3_context c, Z3_error_handler h);
6062-
#endif
60636058

60646059
/**
60656060
\brief Set an error.

0 commit comments

Comments
 (0)