diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 1646c691f..66002baa0 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -319,6 +319,15 @@ extern "C" { 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) { Z3_TRY; LOG_Z3_func_interp_get_arity(c, f); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index cf1a5070a..2f67cb72a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1735,6 +1735,10 @@ namespace z3 { Z3_add_func_entry(ctx(), m_interp, args, value); check_error(); } + void set_else(expr& value) { + Z3_func_entry_set_else(ctx(), m_interp, value); + check_error(); + } }; class model : public object { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 2f14c3f2e..045417d38 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4925,6 +4925,16 @@ extern "C" { */ 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.