From 3bfc3437f188394e246eed1668fdaef1e8ad8438 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 11:57:13 -0700 Subject: [PATCH 1/2] purify Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 36 ++++----------- src/ast/arith_decl_plugin.h | 46 +++++-------------- src/ast/rewriter/arith_rewriter.cpp | 7 +-- .../simplifier/arith_simplifier_plugin.cpp | 2 - src/qe/nlqsat.cpp | 12 +---- src/smt/theory_arith_core.h | 17 ++++--- src/smt/theory_lra.cpp | 10 ++-- src/tactic/arith/purify_arith_tactic.cpp | 15 +++--- 8 files changed, 44 insertions(+), 101 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 01b671c99..03ee77458 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -215,18 +215,8 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { m_e = m->mk_const(e_decl); m->inc_ref(m_e); - func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); - m_0_pw_0_int = m->mk_const(z_pw_z_int); - m->inc_ref(m_0_pw_0_int); - - func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); - m_0_pw_0_real = m->mk_const(z_pw_z_real); - m->inc_ref(m_0_pw_0_real); MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); - MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); - MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); - MK_UNARY(m_mod_0_decl, "mod0", OP_MOD_0, i); MK_UNARY(m_u_asin_decl, "asin-u", OP_U_ASIN, r); MK_UNARY(m_u_acos_decl, "acos-u", OP_U_ACOS, r); } @@ -279,12 +269,7 @@ arith_decl_plugin::arith_decl_plugin(): m_atanh_decl(0), m_pi(0), m_e(0), - m_0_pw_0_int(0), - m_0_pw_0_real(0), m_neg_root_decl(0), - m_div_0_decl(0), - m_idiv_0_decl(0), - m_mod_0_decl(0), m_u_asin_decl(0), m_u_acos_decl(0), m_convert_int_numerals_to_real(false) { @@ -339,12 +324,7 @@ void arith_decl_plugin::finalize() { DEC_REF(m_atanh_decl); DEC_REF(m_pi); DEC_REF(m_e); - DEC_REF(m_0_pw_0_int); - DEC_REF(m_0_pw_0_real); DEC_REF(m_neg_root_decl); - DEC_REF(m_div_0_decl); - DEC_REF(m_idiv_0_decl); - DEC_REF(m_mod_0_decl); DEC_REF(m_u_asin_decl); DEC_REF(m_u_acos_decl); m_manager->dec_array_ref(m_small_ints.size(), m_small_ints.c_ptr()); @@ -392,12 +372,12 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_ATANH: return m_atanh_decl; case OP_PI: return m_pi->get_decl(); case OP_E: return m_e->get_decl(); - case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl(); - case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl(); + //case OP_0_PW_0_INT: return m_0_pw_0_int->get_decl(); + //case OP_0_PW_0_REAL: return m_0_pw_0_real->get_decl(); case OP_NEG_ROOT: return m_neg_root_decl; - case OP_DIV_0: return m_div_0_decl; - case OP_IDIV_0: return m_idiv_0_decl; - case OP_MOD_0: return m_mod_0_decl; + //case OP_DIV_0: return m_div_0_decl; + //case OP_IDIV_0: return m_idiv_0_decl; + //case OP_MOD_0: return m_mod_0_decl; case OP_U_ASIN: return m_u_asin_decl; case OP_U_ACOS: return m_u_acos_decl; default: return 0; @@ -489,9 +469,9 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args static bool is_const_op(decl_kind k) { return k == OP_PI || - k == OP_E || - k == OP_0_PW_0_INT || - k == OP_0_PW_0_REAL; + k == OP_E; + //k == OP_0_PW_0_INT || + //k == OP_0_PW_0_REAL; } func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index a66ddd967..4b24ea5e6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -70,12 +70,7 @@ enum arith_op_kind { OP_PI, OP_E, // under-specified symbols - OP_0_PW_0_INT, // 0^0 for integers - OP_0_PW_0_REAL, // 0^0 for reals OP_NEG_ROOT, // x^n when n is even and x is negative - OP_DIV_0, // x/0 - OP_IDIV_0, // x div 0 - OP_MOD_0, // x mod 0 OP_U_ASIN, // asin(x) for x < -1 or x > 1 OP_U_ACOS, // acos(x) for x < -1 or x > 1 LAST_ARITH_OP @@ -141,12 +136,7 @@ protected: app * m_pi; app * m_e; - app * m_0_pw_0_int; - app * m_0_pw_0_real; func_decl * m_neg_root_decl; - func_decl * m_div_0_decl; - func_decl * m_idiv_0_decl; - func_decl * m_mod_0_decl; func_decl * m_u_asin_decl; func_decl * m_u_acos_decl; ptr_vector m_small_ints; @@ -207,10 +197,6 @@ public: app * mk_e() const { return m_e; } - app * mk_0_pw_0_int() const { return m_0_pw_0_int; } - - app * mk_0_pw_0_real() const { return m_0_pw_0_real; } - virtual expr * get_some_value(sort * s); virtual bool is_considered_uninterpreted(func_decl * f) { @@ -218,12 +204,7 @@ public: return false; switch (f->get_decl_kind()) { - case OP_0_PW_0_INT: - case OP_0_PW_0_REAL: case OP_NEG_ROOT: - case OP_DIV_0: - case OP_IDIV_0: - case OP_MOD_0: case OP_U_ASIN: case OP_U_ACOS: return true; @@ -276,9 +257,9 @@ public: bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); } bool is_mul(expr const * n) const { return is_app_of(n, m_afid, OP_MUL); } bool is_div(expr const * n) const { return is_app_of(n, m_afid, OP_DIV); } - bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } + //bool is_div0(expr const * n) const { return is_app_of(n, m_afid, OP_DIV_0); } bool is_idiv(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV); } - bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } + //bool is_idiv0(expr const * n) const { return is_app_of(n, m_afid, OP_IDIV_0); } bool is_mod(expr const * n) const { return is_app_of(n, m_afid, OP_MOD); } bool is_rem(expr const * n) const { return is_app_of(n, m_afid, OP_REM); } bool is_to_real(expr const * n) const { return is_app_of(n, m_afid, OP_TO_REAL); } @@ -389,16 +370,16 @@ public: app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } app * mk_gt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GT, arg1, arg2); } - app * mk_add(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); } - app * mk_add(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } - app * mk_add(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } + app * mk_add(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_ADD, num_args, args); } + app * mk_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2); } + app * mk_add(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_ADD, arg1, arg2, arg3); } - app * mk_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } - app * mk_sub(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } - app * mk_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); } - app * mk_mul(expr * arg1, expr * arg2, expr* arg3) { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); } - app * mk_mul(unsigned num_args, expr * const * args) { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); } - app * mk_uminus(expr * arg) { return m_manager.mk_app(m_afid, OP_UMINUS, arg); } + app * mk_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_SUB, arg1, arg2); } + app * mk_sub(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_SUB, num_args, args); } + app * mk_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2); } + app * mk_mul(expr * arg1, expr * arg2, expr* arg3) const { return m_manager.mk_app(m_afid, OP_MUL, arg1, arg2, arg3); } + app * mk_mul(unsigned num_args, expr * const * args) const { return m_manager.mk_app(m_afid, OP_MUL, num_args, args); } + app * mk_uminus(expr * arg) const { return m_manager.mk_app(m_afid, OP_UMINUS, arg); } app * mk_div(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_DIV, arg1, arg2); } app * mk_idiv(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_IDIV, arg1, arg2); } app * mk_rem(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_REM, arg1, arg2); } @@ -425,11 +406,6 @@ public: app * mk_pi() { return plugin().mk_pi(); } app * mk_e() { return plugin().mk_e(); } - app * mk_0_pw_0_int() { return plugin().mk_0_pw_0_int(); } - app * mk_0_pw_0_real() { return plugin().mk_0_pw_0_real(); } - app * mk_div0(expr * arg) { return m_manager.mk_app(m_afid, OP_DIV_0, arg); } - app * mk_idiv0(expr * arg) { return m_manager.mk_app(m_afid, OP_IDIV_0, arg); } - app * mk_mod0(expr * arg) { return m_manager.mk_app(m_afid, OP_MOD_0, arg); } app * mk_neg_root(expr * arg1, expr * arg2) { return m_manager.mk_app(m_afid, OP_NEG_ROOT, arg1, arg2); } app * mk_u_asin(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ASIN, arg); } app * mk_u_acos(expr * arg) { return m_manager.mk_app(m_afid, OP_U_ACOS, arg); } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 18556b71b..fc9b1ac1d 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -680,8 +680,7 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul if (m_util.is_numeral(arg2, v2, is_int)) { SASSERT(!is_int); if (v2.is_zero()) { - result = m_util.mk_div0(arg1); - return BR_REWRITE1; + return BR_FAILED; } else if (m_util.is_numeral(arg1, v1, is_int)) { result = m_util.mk_numeral(v1/v2, false); @@ -734,10 +733,6 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_numeral(div(v1, v2), is_int); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { - result = m_util.mk_idiv0(arg1); - return BR_REWRITE1; - } return BR_FAILED; } diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index 8410ce143..bfe72b232 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -405,8 +405,6 @@ bool arith_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * co case OP_POWER: return false; case OP_ABS: SASSERT(num_args == 1); mk_abs(args[0], result); break; case OP_IRRATIONAL_ALGEBRAIC_NUM: return false; - case OP_DIV_0: return false; - case OP_IDIV_0: return false; default: return false; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 0f2437982..3e5a9f24f 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -444,16 +444,12 @@ namespace qe { div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m), m_zero(a.mk_real(0), m) {} ~div_rewriter_cfg() {} br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) { - if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1])) { + rational r; + if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && (!a.is_numeral(args[1], r) || r.is_zero())) { result = m.mk_fresh_const("div", a.mk_real()); m_divs.push_back(div(m, args[0], args[1], to_app(result))); return BR_DONE; } - if (is_decl_of(f, a.get_family_id(), OP_DIV_0) && sz == 1 && !a.is_numeral(args[0])) { - result = m.mk_fresh_const("div", a.mk_real()); - m_divs.push_back(div(m, args[0], m_zero, to_app(result))); - return BR_DONE; - } return BR_FAILED; } vector
const& divs() const { return m_divs; } @@ -507,10 +503,6 @@ namespace qe { m_has_divs = true; return; } - if (a.is_div0(n) && s.m_mode == qsat_t) { - m_has_divs = true; - return; - } TRACE("qe", tout << "not NRA: " << mk_pp(n, s.m) << "\n";); throw tactic_exception("not NRA"); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index a30e51133..b5e7db310 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -395,7 +395,8 @@ namespace smt { template theory_var theory_arith::internalize_div(app * n) { - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); @@ -406,7 +407,8 @@ namespace smt { template theory_var theory_arith::internalize_idiv(app * n) { - found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); app * mod = m_util.mk_mod(n->get_arg(0), n->get_arg(1)); @@ -419,7 +421,8 @@ namespace smt { template theory_var theory_arith::internalize_mod(app * n) { TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";); - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); if (!ctx.relevancy()) @@ -429,7 +432,8 @@ namespace smt { template theory_var theory_arith::internalize_rem(app * n) { - if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n); + rational r; + if (!m_util.is_numeral(n->get_arg(1), r) || r.is_zero()) found_underspecified_op(n); theory_var s = mk_binary_op(n); context & ctx = get_context(); if (!ctx.relevancy()) { @@ -734,11 +738,6 @@ namespace smt { return internalize_div(n); else if (m_util.is_idiv(n)) return internalize_idiv(n); - else if (is_app_of(n, get_id(), OP_IDIV_0) || is_app_of(n, get_id(), OP_DIV_0)) { - ctx.internalize(n->get_arg(0), false); - enode * e = mk_enode(n); - return mk_var(e); - } else if (m_util.is_mod(n)) return internalize_mod(n); else if (m_util.is_rem(n)) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 124fea910..c5e3ae350 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -292,9 +292,6 @@ namespace smt { } void found_not_handled(expr* n) { - if (a.is_div0(n)) { - return; - } m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { m_underspecified.push_back(to_app(n)); @@ -379,7 +376,12 @@ namespace smt { } else if (is_app(n) && a.get_family_id() == to_app(n)->get_family_id()) { app* t = to_app(n); - found_not_handled(n); + if (a.is_div(n, n1, n2) && is_numeral(n2, r)) { + // skip + } + else { + found_not_handled(n); + } internalize_args(t); mk_enode(t); theory_var v = mk_var(n); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 0443a51ed..7e89794ce 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -297,11 +297,11 @@ struct purify_arith_proc { push_cnstr(OR(EQ(y, mk_real_zero()), EQ(u().mk_mul(y, k), x))); push_cnstr_pr(result_pr); - - if (complete()) { + rational r; + if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), - EQ(k, u().mk_div0(x)))); + EQ(k, u().mk_div(x, mk_real_zero())))); push_cnstr_pr(result_pr); } } @@ -348,11 +348,12 @@ struct purify_arith_proc { push_cnstr(OR(u().mk_ge(y, zero), u().mk_lt(k2, u().mk_mul(u().mk_numeral(rational(-1), true), y)))); push_cnstr_pr(mod_pr); - if (complete()) { - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv0(x)))); + rational r; + if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero)))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod0(x)))); + push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero)))); push_cnstr_pr(mod_pr); } } @@ -414,7 +415,7 @@ struct purify_arith_proc { // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); - push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, is_int ? u().mk_0_pw_0_int() : u().mk_0_pw_0_real()))); + push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, u().mk_power(zero, zero)))); push_cnstr_pr(result_pr); } else if (!is_int) { From ce8443581d31b4194f6db010d91f9dab8ee55aac Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Aug 2017 12:15:27 -0700 Subject: [PATCH 2/2] 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.