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

update names

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-27 13:02:59 -07:00
parent f76815a009
commit 03f263b974
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);
}
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);

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; }
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();
}
};

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
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.