mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix naming for functions #1223

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-27 13:00:43 -07:00
parent ce8443581d
commit 623cd5ded2
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_model.cpp
View file

@ -337,9 +337,9 @@ extern "C" {
Z3_CATCH_RETURN(0); 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; 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(fi, void);
//CHECK_NON_NULL(args, void); //CHECK_NON_NULL(args, void);
//CHECK_NON_NULL(value, void); //CHECK_NON_NULL(value, void);

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

@ -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; } 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); } 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) { 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(); check_error();
} }
void set_else(expr& value) { 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(); check_error();
} }
}; };

4
src/api/z3_api.h
View file

@ -4954,9 +4954,9 @@ extern "C" {
If an two entries are added with the same arguments, only the second insertion survives and the If an two entries are added with the same arguments, only the second insertion survives and the
first inserted entry is removed. 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. \brief Increment the reference counter of the given Z3_func_entry object.