mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

expose Z3_model_has_interp to C API

Browse source
This commit is contained in:
Tim Felgentreff 2013-04-09 11:44:16 +02:00
parent 89c1785b73
commit 8fb7de5110
2 changed files with 21 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_model.cpp
View file

@ -62,6 +62,18 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_model_has_interp(Z3_context c, Z3_model m, Z3_func_decl a) {
Z3_TRY;
LOG_Z3_model_has_interp(c, m, a);
CHECK_NON_NULL(m, 0);
if (to_model_ref(m)->has_interpretation(to_func_decl(a))) {
return Z3_TRUE;
} else {
return Z3_FALSE;
}
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f) {
Z3_TRY;
LOG_Z3_model_get_func_interp(c, m, f);

9
src/api/z3_api.h
View file

@ -4455,6 +4455,15 @@ END_MLAPI_EXCLUDE
*/
Z3_ast_opt Z3_API Z3_model_get_const_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
/**
\brief Test if there exists an interpretation (i.e., assignment) of constant \c a in the model \c m.
\pre Z3_get_arity(c, a) == 0
def_API('Z3_model_has_interp', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL)))
*/
Z3_bool Z3_API Z3_model_has_interp(__in Z3_context c, __in Z3_model m, __in Z3_func_decl a);
/**
\brief Return the interpretation of the function \c f in the model \c m.
Return \mlonly [None], \endmlonly \conly \c NULL,