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

add API methods for creating and modifying models, #1223

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

63
src/api/api_model.cpp
View file

@ -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);

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

@ -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; }

54
src/api/z3_api.h
View file

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