mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

change default output to print objective value

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-20 17:11:46 +01:00
parent e3c35840bb
commit d9f3625f93
3 changed files with 31 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/maxcore.cpp
View file

@ -877,6 +877,7 @@ public:
void max_resolve_rc2(exprs const& core, rational weight) { void max_resolve_rc2(exprs const& core, rational weight) {
expr_ref_vector ncore(m); expr_ref_vector ncore(m);
for (expr* f : core) { for (expr* f : core) {
ncore.push_back(mk_not(m, f));
bound_info b; bound_info b;
if (!m_bounds.find(f, b)) if (!m_bounds.find(f, b))
continue; continue;
@ -886,7 +887,6 @@ public:
expr_ref_vector es(m, b.es.size(), b.es.data()); expr_ref_vector es(m, b.es.size(), b.es.data());
expr* amk = mk_atmost(es, b.k + 1, b.weight); expr* amk = mk_atmost(es, b.k + 1, b.weight);
new_assumption(amk, b.weight); new_assumption(amk, b.weight);
ncore.push_back(mk_not(m, f));
m_unfold_upper -= b.weight; m_unfold_upper -= b.weight;
} }
if (core.size() > 1) { if (core.size() > 1) {

20
src/opt/opt_context.cpp
View file

@ -703,25 +703,25 @@ namespace opt {
void context::update_solver() { void context::update_solver() {
sat_params p(m_params); sat_params p(m_params);
if (p.euf()) if (!p.euf() && (!m_enable_sat || !probe_fd()))
return; return;
if (!p.euf()) {
if (!m_enable_sat || !probe_fd()) {
return;
}
if (m_maxsat_engine != symbol("maxres") && if (m_maxsat_engine != symbol("maxres") &&
m_maxsat_engine != symbol("rc2") &&
m_maxsat_engine != symbol("maxres-bin") &&
m_maxsat_engine != symbol("maxres-bin-delay") &&
m_maxsat_engine != symbol("pd-maxres") && m_maxsat_engine != symbol("pd-maxres") &&
m_maxsat_engine != symbol("bcd2") && m_maxsat_engine != symbol("bcd2") &&
m_maxsat_engine != symbol("sls")) { m_maxsat_engine != symbol("sls")) {
return; return;
} }
if (opt_params(m_params).priority() == symbol("pareto")) {
if (opt_params(m_params).priority() == symbol("pareto"))
return; return;
}
if (m.proofs_enabled()) { if (m.proofs_enabled())
return; return;
}
}
m_params.set_bool("minimize_core_partial", true); m_params.set_bool("minimize_core_partial", true);
m_params.set_bool("minimize_core", true); m_params.set_bool("minimize_core", true);
m_sat_solver = mk_inc_sat_solver(m, m_params); m_sat_solver = mk_inc_sat_solver(m, m_params);

16
src/shell/opt_frontend.cpp
View file

@ -33,9 +33,14 @@ static void display_model(std::ostream& out) {
return; return;
model_ref mdl; model_ref mdl;
g_opt->get_model(mdl); g_opt->get_model(mdl);
if (mdl) { if (mdl)
model_smt2_pp(out, g_opt->get_manager(), *mdl, 0); model_smt2_pp(out, g_opt->get_manager(), *mdl, 0);
} }
static void display_objective() {
if (!g_opt)
return;
std::ostream& out = std::cout;
for (unsigned h : g_handles) { for (unsigned h : g_handles) {
expr_ref lo = g_opt->get_lower(h); expr_ref lo = g_opt->get_lower(h);
expr_ref hi = g_opt->get_upper(h); expr_ref hi = g_opt->get_upper(h);
@ -48,14 +53,12 @@ static void display_model(std::ostream& out) {
} }
} }
static void display_model() { static void display_model() {
if (g_display_model) if (g_display_model)
display_model(std::cout); display_model(std::cout);
} }
static void display_results() {
IF_VERBOSE(1, display_model(verbose_stream()));
}
static void display_statistics() { static void display_statistics() {
lock_guard lock(*display_stats_mux); lock_guard lock(*display_stats_mux);
@ -66,8 +69,6 @@ static void display_statistics() {
double end_time = static_cast<double>(clock()); double end_time = static_cast<double>(clock());
std::cout << "time: " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n"; std::cout << "time: " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n";
} }
display_results();
} }
static void STD_CALL on_ctrl_c(int) { static void STD_CALL on_ctrl_c(int) {
@ -136,6 +137,7 @@ static unsigned parse_opt(std::istream& in, opt_format f) {
} }
display_statistics(); display_statistics();
display_model(); display_model();
display_objective();
g_opt = nullptr; g_opt = nullptr;
return 0; return 0;
} }