From 4719aa11bb15b4e5f7e8ce3fdb0f3353d0c4a2a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Dec 2013 17:00:34 -0800 Subject: [PATCH] backfilling API functions Signed-off-by: Nikolaj Bjorner --- src/api/api_opt.cpp | 102 +++++++++++++++++++++++++++++----- src/api/z3_api.h | 132 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 220 insertions(+), 14 deletions(-) diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 4f9609840..497f988cf 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -21,6 +21,8 @@ Revision History: #include"api_context.h" #include"api_util.h" #include"opt_context.h" +#include"cancel_eh.h" +#include"scoped_timer.h" extern "C" { @@ -31,55 +33,127 @@ extern "C" { }; inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast(o); } inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast(o); } + inline opt::context& to_optimize_ref(Z3_optimize o) { return *to_optimize(o)->m_opt; } Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) { - return 0; + Z3_TRY; + LOG_Z3_mk_optimize(c); + RESET_ERROR_CODE(); + Z3_optimize_ref * o = alloc(Z3_optimize_ref); + o->m_opt = alloc(opt::context,mk_c(c)->m()); + mk_c(c)->save_object(o); + RETURN_Z3(of_optimize(o)); + Z3_CATCH_RETURN(0); } void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize o) { - + Z3_TRY; + LOG_Z3_optimize_inc_ref(c, o); + RESET_ERROR_CODE(); + to_optimize(o)->inc_ref(); + Z3_CATCH; } void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) { - + Z3_TRY; + LOG_Z3_optimize_dec_ref(c, o); + RESET_ERROR_CODE(); + to_optimize(o)->dec_ref(); + Z3_CATCH; } void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a) { - + Z3_TRY; + LOG_Z3_optimize_assert(c, o, a); + RESET_ERROR_CODE(); + CHECK_FORMULA(a,); + to_optimize_ref(o).add_hard_constraint(to_expr(a)); + Z3_CATCH; } void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) { - + Z3_TRY; + LOG_Z3_optimize_assert_soft(c, o, a, weight, id); + RESET_ERROR_CODE(); + CHECK_FORMULA(a,); + rational w("weight"); + to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id)); + Z3_CATCH; } - void Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t) { - + void Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) { + Z3_TRY; + LOG_Z3_optimize_maximize(c, o, t); + RESET_ERROR_CODE(); + CHECK_VALID_AST(t,); + to_optimize_ref(o).add_objective(to_app(t), true); + Z3_CATCH; } - void Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t) { - + void Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) { + Z3_TRY; + LOG_Z3_optimize_minimize(c, o, t); + RESET_ERROR_CODE(); + CHECK_VALID_AST(t,); + to_optimize_ref(o).add_objective(to_app(t), false); + Z3_CATCH; } - Z3_lbool Z3_API Z3_optimize_check(Z3_context c) { - return Z3_L_UNDEF; + Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_check(c, o); + RESET_ERROR_CODE(); + lbool r = l_undef; + cancel_eh eh(to_optimize_ref(o)); + unsigned timeout = 0; // to_optimize(o)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + api::context::set_interruptable si(*(mk_c(c)), eh); + { + scoped_timer timer(timeout, &eh); + try { + r = to_optimize_ref(o).optimize(); + } + catch (z3_exception& ex) { + mk_c(c)->handle_exception(ex); + r = l_undef; + } + // to_optimize_ref(d).cleanup(); + } + return of_lbool(r); + Z3_CATCH_RETURN(Z3_L_UNDEF); } void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p) { - + Z3_TRY; + LOG_Z3_optimize_set_params(c, o, p); + RESET_ERROR_CODE(); + param_descrs descrs; + to_optimize_ref(o).collect_param_descrs(descrs); + to_params(p)->m_params.validate(descrs); + to_optimize_ref(o).updt_params(to_param_ref(p)); + Z3_CATCH; } Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o) { - return 0; + Z3_TRY; + LOG_Z3_optimize_get_param_descrs(c, o); + RESET_ERROR_CODE(); + Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref); + mk_c(c)->save_object(d); + to_optimize_ref(o).collect_param_descrs(d->m_descrs); + Z3_param_descrs r = of_param_descrs(d); + RETURN_Z3(r); + Z3_CATCH_RETURN(0); } - // get lower value or current approximation Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx) { + NOT_IMPLEMENTED_YET(); return 0; } // get upper or current approximation Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx) { + NOT_IMPLEMENTED_YET(); return 0; } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d7fea33d7..f6064d543 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -86,6 +86,7 @@ DEFINE_VOID(Z3_theory_data); - \c Z3_func_interp: interpretation of a function in a model. - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point. - \c Z3_fixedpoint: context for the recursive predicate solver. + - \c Z3_optimize: context for solving optimization queries. - \c Z3_ast_vector: vector of \c Z3_ast objects. - \c Z3_ast_map: mapping from \c Z3_ast to \c Z3_ast objects. - \c Z3_goal: set of formulas that can be solved and/or transformed using tactics and solvers. @@ -1205,6 +1206,7 @@ typedef enum def_Type('FUNC_INTERP', 'Z3_func_interp', 'FuncInterpObj') def_Type('FUNC_ENTRY', 'Z3_func_entry', 'FuncEntryObj') def_Type('FIXEDPOINT', 'Z3_fixedpoint', 'FixedpointObj') + def_Type('OPTIMIZE', 'Z3_optimize', 'OptimizeObj') def_Type('PARAM_DESCRS', 'Z3_param_descrs', 'ParamDescrs') def_Type('RCF_NUM', 'Z3_rcf_num', 'RCFNumObj') */ @@ -5935,6 +5937,136 @@ END_MLAPI_EXCLUDE #endif #endif + + +#ifdef CorML4 + /** + @name Optimize facilities + */ + /*@{*/ + + /** + \brief Create a new optimize context. + + \conly \remark User must use #Z3_optimize_inc_ref and #Z3_optimize_dec_ref to manage optimize objects. + \conly Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. + + def_API('Z3_mk_optimize', OPTIMIZE, (_in(CONTEXT), )) + */ + Z3_optimize Z3_API Z3_mk_optimize(__in Z3_context c); + +#ifdef Conly + /** + \brief Increment the reference counter of the given optimize context + + def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE))) + */ + void Z3_API Z3_optimize_inc_ref(__in Z3_context c,__in Z3_optimize d); + + /** + \brief Decrement the reference counter of the given optimize context. + + def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE))) + */ + void Z3_API Z3_optimize_dec_ref(__in Z3_context c,__in Z3_optimize d); +#endif + + /** + \brief Assert hard constraint to the optimization context. + + def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) + */ + void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a); + + + /** + \brief Assert soft constraint to the optimization context. + \param c - context + \param o - optimization context + \param a - formula + \param weight - a positive weight, penalty for violating soft constraint + \param id - optional identifier to group soft constraints + + def_API('Z3_optimize_assert_soft', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL))) + */ + void Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id); + + + /** + \brief Add a maximiztion constraint. + \param c - context + \param o - optimization context + \param a - arithmetical term + def_API('Z3_optimize_maximize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) + */ + void Z3_API Z3_optimize_maximize(Z3_context, Z3_optimize o, Z3_ast t); + + /** + \brief Add a minimiztion constraint. + \param c - context + \param o - optimization context + \param a - arithmetical term + + def_API('Z3_optimize_minimize', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) + */ + void Z3_API Z3_optimize_minimize(Z3_context, Z3_optimize o, Z3_ast t); + + /** + \brief Check consistency and produce optimal values. + \param c - context + \param o - optimization context + + def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o); + + + /** + \brief Set parameters on optimization context. + + \param c - context + \param o - optimization context + \param p - parameters + + def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS))) + */ + void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p); + + /** + \brief Return the parameter description set for the given optimize object. + + \param c - context + \param o - optimization context + + def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o); + + /** + \brief Retrieve lower bound value or approximation for the i'th optimization objective. + + \param c - context + \param o - optimization context + \param idx - index of optimization objective + + def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) + */ + Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx); + + /** + \brief Retrieve upper bound value or approximation for the i'th optimization objective. + + \param c - context + \param o - optimization context + \param idx - index of optimization objective + + def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) + */ + Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx); + + +#endif + #ifdef CorML4 /*@}*/