From a206362cef8a6dce748f73a14f3aaec8ec14456c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 22 Aug 2017 11:41:25 -0700 Subject: [PATCH] add comments addressing some questions #1223 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 46c8fbb30..bea40f30a 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4862,9 +4862,14 @@ extern "C" { \brief Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0. + \param c context + \param m model + \param f function declaration + \param default_value default value for function interpretation + def_API('Z3_add_func_interp', FUNC_INTERP, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST))) */ - Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val); + Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value); /** \brief Add a constant interpretation. @@ -4930,6 +4935,15 @@ extern "C" { /** \brief add a function entry to a function interpretation. + \param c logical context + \param fi a function interpregation to be updated. + \param args list of arguments. They should be constant values (such as integers) and be of the same types as the domain of the function. + \param value value of the function when the parameters match args. + + It is assumed that entries added to a function cover disjoint arguments. + 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))) */ void Z3_API Z3_add_func_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);