From 03f263b974a8300444a956877940c9967a425b3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 13:02:59 -0700 Subject: [PATCH] update names Signed-off-by: Nikolaj Bjorner --- src/api/api_model.cpp | 4 ++-- src/api/c++/z3++.h | 4 ++-- src/api/z3_api.h | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 66002baa0..540f014c6 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -337,9 +337,9 @@ extern "C" { Z3_CATCH_RETURN(0); } - void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) { + void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value) { Z3_TRY; - LOG_Z3_add_func_entry(c, fi, args, value); + LOG_Z3_func_interp_add_entry(c, fi, args, value); //CHECK_NON_NULL(fi, void); //CHECK_NON_NULL(args, void); //CHECK_NON_NULL(value, void); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 2f67cb72a..6d8ff3b35 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1732,11 +1732,11 @@ namespace z3 { unsigned num_entries() const { unsigned r = Z3_func_interp_get_num_entries(ctx(), m_interp); check_error(); return r; } func_entry entry(unsigned i) const { Z3_func_entry e = Z3_func_interp_get_entry(ctx(), m_interp, i); check_error(); return func_entry(ctx(), e); } void add_entry(expr_vector const& args, expr& value) { - Z3_add_func_entry(ctx(), m_interp, args, value); + Z3_func_interp_add_entry(ctx(), m_interp, args, value); check_error(); } void set_else(expr& value) { - Z3_func_entry_set_else(ctx(), m_interp, value); + Z3_func_interp_set_else(ctx(), m_interp, value); check_error(); } }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 045417d38..bed70cb6c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4954,9 +4954,9 @@ extern "C" { If an two entries are added with the same arguments, only the second insertion survives and the first inserted entry is removed. - def_API('Z3_add_func_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST))) + def_API('Z3_func_interp_add_entry', VOID, (_in(CONTEXT), _in(FUNC_INTERP), _in(AST_VECTOR), _in(AST))) */ - void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value); + void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value); /** \brief Increment the reference counter of the given Z3_func_entry object.