From ce8443581d31b4194f6db010d91f9dab8ee55aac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 12:15:27 -0700 Subject: [PATCH] add API methods for creating and modifying models, #1223 Signed-off-by: Nikolaj Bjorner --- src/api/api_model.cpp | 63 +++++++++++++++++++++++++++++++++++++++++++ src/api/c++/z3++.h | 20 ++++++++++++++ src/api/z3_api.h | 54 +++++++++++++++++++++++++++++++++++++ 3 files changed, 137 insertions(+) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index de917650d..66002baa0 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -30,6 +30,17 @@ Revision History: extern "C" { + Z3_model Z3_API Z3_mk_model(Z3_context c) { + Z3_TRY; + LOG_Z3_mk_model(c); + RESET_ERROR_CODE(); + Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); + m_ref->m_model = alloc(model, mk_c(c)->m()); + mk_c(c)->save_object(m_ref); + RETURN_Z3(of_model(m_ref)); + Z3_CATCH_RETURN(0); + } + void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m) { Z3_TRY; LOG_Z3_model_inc_ref(c, m); @@ -224,6 +235,31 @@ extern "C" { Z3_CATCH_RETURN(0); } + Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast else_val) { + Z3_TRY; + LOG_Z3_add_func_interp(c, m, f, else_val); + RESET_ERROR_CODE(); + func_decl* d = to_func_decl(f); + model* mdl = to_model_ref(m); + Z3_func_interp_ref * f_ref = alloc(Z3_func_interp_ref, *mk_c(c), mdl); + f_ref->m_func_interp = alloc(func_interp, mk_c(c)->m(), d->get_arity()); + mk_c(c)->save_object(f_ref); + mdl->register_decl(d, f_ref->m_func_interp); + f_ref->m_func_interp->set_else(to_expr(else_val)); + RETURN_Z3(of_func_interp(f_ref)); + Z3_CATCH_RETURN(0); + } + + void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a) { + Z3_TRY; + LOG_Z3_add_const_interp(c, m, f, a); + RESET_ERROR_CODE(); + func_decl* d = to_func_decl(f); + model* mdl = to_model_ref(m); + mdl->register_decl(d, to_expr(a)); + Z3_CATCH; + } + void Z3_API Z3_func_interp_inc_ref(Z3_context c, Z3_func_interp f) { Z3_TRY; LOG_Z3_func_interp_inc_ref(c, f); @@ -283,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); @@ -292,6 +337,24 @@ 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) { + Z3_TRY; + LOG_Z3_add_func_entry(c, fi, args, value); + //CHECK_NON_NULL(fi, void); + //CHECK_NON_NULL(args, void); + //CHECK_NON_NULL(value, void); + func_interp* _fi = to_func_interp_ref(fi); + expr* _value = to_expr(value); + if (to_ast_vector_ref(args).size() != _fi->get_arity()) { + SET_ERROR_CODE(Z3_IOB); + return; + } + // check sorts of value + expr* const* _args = (expr* const*) to_ast_vector_ref(args).c_ptr(); + _fi->insert_entry(_args, _value); + Z3_CATCH; + } + void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e) { Z3_TRY; LOG_Z3_func_entry_inc_ref(c, e); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 42db6f352..2f67cb72a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1731,6 +1731,14 @@ namespace z3 { expr else_value() const { Z3_ast r = Z3_func_interp_get_else(ctx(), m_interp); check_error(); return expr(ctx(), 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); } + void add_entry(expr_vector const& args, expr& value) { + 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 { @@ -1740,6 +1748,7 @@ namespace z3 { Z3_model_inc_ref(ctx(), m); } public: + model(context & c):object(c) { init(Z3_mk_model(c)); } model(context & c, Z3_model m):object(c) { init(m); } model(model const & s):object(s) { init(s.m_model); } ~model() { Z3_model_dec_ref(ctx(), m_model); } @@ -1795,6 +1804,17 @@ namespace z3 { return 0 != Z3_model_has_interp(ctx(), m_model, f); } + func_interp add_func_interp(func_decl& f, expr& else_val) { + Z3_func_interp r = Z3_add_func_interp(ctx(), m_model, f, else_val); + check_error(); + return func_interp(ctx(), r); + } + + void add_const_interp(func_decl& f, expr& value) { + Z3_add_const_interp(ctx(), m_model, f, value); + check_error(); + } + friend std::ostream & operator<<(std::ostream & out, model const & m); }; inline std::ostream & operator<<(std::ostream & out, model const & m) { out << Z3_model_to_string(m.ctx(), m); return out; } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 43c175ca8..045417d38 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4680,6 +4680,14 @@ extern "C" { /** @name Models */ /*@{*/ + + /** + \brief Create a fresh model object. It has reference count 0. + + def_API('Z3_mk_model', MODEL, (_in(CONTEXT),)) + */ + Z3_model Z3_API Z3_mk_model(Z3_context c); + /** \brief Increment the reference counter of the given model. @@ -4850,6 +4858,26 @@ extern "C" { */ Z3_func_decl Z3_API Z3_get_as_array_func_decl(Z3_context c, Z3_ast a); + /** + \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 default_value); + + /** + \brief Add a constant interpretation. + + def_API('Z3_add_const_interp', VOID, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(AST))) + */ + void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a); + /** \brief Increment the reference counter of the given Z3_func_interp object. @@ -4897,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. @@ -4904,6 +4942,22 @@ extern "C" { */ unsigned Z3_API Z3_func_interp_get_arity(Z3_context c, Z3_func_interp f); + /** + \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); + /** \brief Increment the reference counter of the given Z3_func_entry object.