mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-27 12:19:24 -07:00
parent d940516df3
commit f9dc6385b2
3 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_model.cpp
View file

@ -319,6 +319,15 @@ extern "C" {
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value) {
Z3_TRY;
LOG_Z3_func_interp_set_else(c, f, else_value);
RESET_ERROR_CODE();
// CHECK_NON_NULL(f, 0);
to_func_interp_ref(f)->set_else(to_expr(else_value));
Z3_CATCH;
}
unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f) { unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f) {
Z3_TRY; Z3_TRY;
LOG_Z3_func_interp_get_arity(c, f); LOG_Z3_func_interp_get_arity(c, f);

4
src/api/c++/z3++.h
View file

@ -1735,6 +1735,10 @@ namespace z3 {
Z3_add_func_entry(ctx(), m_interp, args, value); Z3_add_func_entry(ctx(), m_interp, args, value);
check_error(); check_error();
} }
void set_else(expr& value) {
Z3_func_entry_set_else(ctx(), m_interp, value);
check_error();
}
}; };
class model : public object { class model : public object {

10
src/api/z3_api.h
View file

@ -4925,6 +4925,16 @@ extern "C" {
*/ */
Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f); Z3_ast Z3_API Z3_func_interp_get_else(Z3_context c, Z3_func_interp f);
/**
\brief Return the 'else' value of the given function interpretation.
A function interpretation is represented as a finite map and an 'else' value.
This procedure can be used to update the 'else' value.
def_API('Z3_func_interp_set_else', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST)))
*/
void Z3_API Z3_func_interp_set_else(Z3_context c, Z3_func_interp f, Z3_ast else_value);
/** /**
\brief Return the arity (number of arguments) of the given function interpretation. \brief Return the arity (number of arguments) of the given function interpretation.