mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

backfilling API functions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-03 17:00:34 -08:00
parent 222d4a8f01
commit 4719aa11bb
2 changed files with 220 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

102
src/api/api_opt.cpp
View file

@ -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<Z3_optimize_ref *>(o); }
inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast<Z3_optimize>(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<opt::context> 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;
}

132
src/api/z3_api.h
View file

@ -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
/*@}*/