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

fix #5515

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-28 18:05:51 -07:00
parent e7fcbd9563
commit b1bc890992
3 changed files with 22 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_opt.cpp
View file

@ -325,6 +325,7 @@ extern "C" {
RESET_ERROR_CODE();
Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
to_optimize_ptr(d)->collect_statistics(st->m_stats);
to_optimize_ptr(d)->collect_timer_stats(st->m_stats);
mk_c(c)->save_object(st);
Z3_stats r = of_stats(st);
RETURN_Z3(r);

1
src/opt/opt_context.cpp
View file

@ -266,6 +266,7 @@ namespace opt {
}
lbool context::optimize(expr_ref_vector const& _asms) {
scoped_time _st(*this);
if (m_pareto) {
return execute_pareto();
}

20
src/opt/opt_context.h
View file

@ -117,6 +117,17 @@ namespace opt {
{}
};
double m_time = 0;
class scoped_time {
context& c;
timer t;
public:
scoped_time(context& c):c(c) { c.m_time = 0; }
~scoped_time() { c.m_time = t.get_seconds(); }
};
class scoped_state {
ast_manager& m;
arith_util m_arith;
@ -261,6 +272,13 @@ namespace opt {
m_on_model_eh = on_model;
}
void collect_timer_stats(statistics& st) const {
if (m_time != 0)
st.update("time", m_time);
}
private:
lbool execute(objective const& obj, bool committed, bool scoped);
lbool execute_min_max(unsigned index, bool committed, bool scoped, bool is_max);
@ -340,6 +358,8 @@ namespace opt {
// quantifiers
bool is_qsat_opt();
lbool run_qsat_opt();
};
}