mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

update timeout logic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-09 22:27:35 -07:00
parent cf55854d22
commit fb0305d5ec
2 changed files with 20 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

38
src/api/api_opt.cpp
View file

@ -36,7 +36,8 @@ extern "C" {
}; };
inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); } 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 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; } inline opt::context* to_optimize_ptr(Z3_optimize o) { return to_optimize(o)->m_opt; }
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) { Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) {
Z3_TRY; Z3_TRY;
@ -70,7 +71,7 @@ extern "C" {
LOG_Z3_optimize_assert(c, o, a); LOG_Z3_optimize_assert(c, o, a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_FORMULA(a,); CHECK_FORMULA(a,);
to_optimize_ref(o)->add_hard_constraint(to_expr(a)); to_optimize_ref(o).add_hard_constraint(to_expr(a));
Z3_CATCH; Z3_CATCH;
} }
@ -80,7 +81,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_FORMULA(a,0); CHECK_FORMULA(a,0);
rational w(weight); rational w(weight);
return to_optimize_ref(o)->add_soft_constraint(to_expr(a), w, to_symbol(id)); return to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -89,7 +90,7 @@ extern "C" {
LOG_Z3_optimize_maximize(c, o, t); LOG_Z3_optimize_maximize(c, o, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t,0); CHECK_VALID_AST(t,0);
return to_optimize_ref(o)->add_objective(to_app(t), true); return to_optimize_ref(o).add_objective(to_app(t), true);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -98,7 +99,7 @@ extern "C" {
LOG_Z3_optimize_minimize(c, o, t); LOG_Z3_optimize_minimize(c, o, t);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
CHECK_VALID_AST(t,0); CHECK_VALID_AST(t,0);
return to_optimize_ref(o)->add_objective(to_app(t), false); return to_optimize_ref(o).add_objective(to_app(t), false);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
} }
@ -107,20 +108,19 @@ extern "C" {
LOG_Z3_optimize_check(c, o); LOG_Z3_optimize_check(c, o);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
lbool r = l_undef; lbool r = l_undef;
cancel_eh<opt::context> eh(*to_optimize_ref(o)); cancel_eh<opt::context> eh(to_optimize_ref(o));
unsigned timeout = 0xFFFFFFF; unsigned timeout = to_optimize_ref(o).get_params().get_uint("timeout", mk_c(c)->get_timeout());
// to_optimize(o)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
api::context::set_interruptable si(*(mk_c(c)), eh); api::context::set_interruptable si(*(mk_c(c)), eh);
{ {
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);
try { try {
r = to_optimize_ref(o)->optimize(); r = to_optimize_ref(o).optimize();
} }
catch (z3_exception& ex) { catch (z3_exception& ex) {
mk_c(c)->handle_exception(ex); mk_c(c)->handle_exception(ex);
r = l_undef; r = l_undef;
} }
// to_optimize_ref(d)->cleanup(); // to_optimize_ref(d).cleanup();
} }
return of_lbool(r); return of_lbool(r);
Z3_CATCH_RETURN(Z3_L_UNDEF); Z3_CATCH_RETURN(Z3_L_UNDEF);
@ -131,7 +131,7 @@ extern "C" {
LOG_Z3_optimize_get_model(c, o); LOG_Z3_optimize_get_model(c, o);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
model_ref _m; model_ref _m;
to_optimize_ref(o)->get_model(_m); to_optimize_ref(o).get_model(_m);
Z3_model_ref * m_ref = alloc(Z3_model_ref); Z3_model_ref * m_ref = alloc(Z3_model_ref);
if (_m) { if (_m) {
m_ref->m_model = _m; m_ref->m_model = _m;
@ -149,10 +149,10 @@ extern "C" {
LOG_Z3_optimize_set_params(c, o, p); LOG_Z3_optimize_set_params(c, o, p);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
param_descrs descrs; param_descrs descrs;
to_optimize_ref(o)->collect_param_descrs(descrs); to_optimize_ref(o).collect_param_descrs(descrs);
to_params(p)->m_params.validate(descrs); to_params(p)->m_params.validate(descrs);
params_ref pr = to_param_ref(p); params_ref pr = to_param_ref(p);
to_optimize_ref(o)->updt_params(pr); to_optimize_ref(o).updt_params(pr);
Z3_CATCH; Z3_CATCH;
} }
@ -162,7 +162,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref); Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
mk_c(c)->save_object(d); mk_c(c)->save_object(d);
to_optimize_ref(o)->collect_param_descrs(d->m_descrs); to_optimize_ref(o).collect_param_descrs(d->m_descrs);
Z3_param_descrs r = of_param_descrs(d); Z3_param_descrs r = of_param_descrs(d);
RETURN_Z3(r); RETURN_Z3(r);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -173,7 +173,7 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_optimize_get_lower(c, o, idx); LOG_Z3_optimize_get_lower(c, o, idx);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
expr_ref e = to_optimize_ref(o)->get_lower(idx); expr_ref e = to_optimize_ref(o).get_lower(idx);
mk_c(c)->save_ast_trail(e); mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_expr(e)); RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -184,7 +184,7 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_optimize_get_upper(c, o, idx); LOG_Z3_optimize_get_upper(c, o, idx);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
expr_ref e = to_optimize_ref(o)->get_upper(idx); expr_ref e = to_optimize_ref(o).get_upper(idx);
mk_c(c)->save_ast_trail(e); mk_c(c)->save_ast_trail(e);
RETURN_Z3(of_expr(e)); RETURN_Z3(of_expr(e));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -194,7 +194,7 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_optimize_to_string(c, o); LOG_Z3_optimize_to_string(c, o);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
return mk_c(c)->mk_external_string(to_optimize_ref(o)->to_string()); return mk_c(c)->mk_external_string(to_optimize_ref(o).to_string());
Z3_CATCH_RETURN(""); Z3_CATCH_RETURN("");
} }
@ -204,7 +204,7 @@ extern "C" {
RESET_ERROR_CODE(); RESET_ERROR_CODE();
std::ostringstream buffer; std::ostringstream buffer;
param_descrs descrs; param_descrs descrs;
to_optimize_ref(d)->collect_param_descrs(descrs); to_optimize_ref(d).collect_param_descrs(descrs);
descrs.display(buffer); descrs.display(buffer);
return mk_c(c)->mk_external_string(buffer.str()); return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN(""); Z3_CATCH_RETURN("");
@ -215,7 +215,7 @@ extern "C" {
LOG_Z3_optimize_get_statistics(c, d); LOG_Z3_optimize_get_statistics(c, d);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
Z3_stats_ref * st = alloc(Z3_stats_ref); Z3_stats_ref * st = alloc(Z3_stats_ref);
to_optimize_ref(d)->collect_statistics(st->m_stats); to_optimize_ref(d).collect_statistics(st->m_stats);
mk_c(c)->save_object(st); mk_c(c)->save_object(st);
Z3_stats r = of_stats(st); Z3_stats r = of_stats(st);
RETURN_Z3(r); RETURN_Z3(r);

1
src/opt/opt_context.h
View file

@ -148,6 +148,7 @@ namespace opt {
void display(std::ostream& out); void display(std::ostream& out);
static void collect_param_descrs(param_descrs & r); static void collect_param_descrs(param_descrs & r);
void updt_params(params_ref& p); void updt_params(params_ref& p);
params_ref& get_params() { return m_params; }
expr_ref get_lower(unsigned idx); expr_ref get_lower(unsigned idx);
expr_ref get_upper(unsigned idx); expr_ref get_upper(unsigned idx);