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

fix #7018

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-28 13:14:44 -08:00
parent 3422f44cea
commit 69f9640fdf
2 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/opt/opt_context.cpp
View file

@ -213,7 +213,7 @@ namespace opt {
void context::add_hard_constraint(expr* f, expr* t) { void context::add_hard_constraint(expr* f, expr* t) {
if (m_calling_on_model) if (m_calling_on_model)
throw default_exception("adding soft constraints is not supported during callbacks"); throw default_exception("adding hard constraints is not supported during callbacks");
m_scoped_state.m_asms.push_back(t); m_scoped_state.m_asms.push_back(t);
m_scoped_state.add(m.mk_implies(t, f)); m_scoped_state.add(m.mk_implies(t, f));
clear_state(); clear_state();
@ -905,12 +905,14 @@ namespace opt {
ptr_vector<expr> deps; ptr_vector<expr> deps;
expr_dependency_ref core(r->dep(i), m); expr_dependency_ref core(r->dep(i), m);
m.linearize(core, deps); m.linearize(core, deps);
if (!deps.empty()) { if (deps.empty())
fmls.push_back(m.mk_implies(m.mk_and(deps.size(), deps.data()), r->form(i)));
}
else {
fmls.push_back(r->form(i)); fmls.push_back(r->form(i));
} else if (deps.size() == 1 && deps[0] == r->form(i))
continue;
else if (is_objective(r->form(i)))
fmls.push_back(r->form(i));
else
fmls.push_back(m.mk_implies(mk_and(m, deps.size(), deps.data()), r->form(i)));
} }
if (r->inconsistent()) { if (r->inconsistent()) {
ptr_vector<expr> core_elems; ptr_vector<expr> core_elems;
@ -920,6 +922,10 @@ namespace opt {
} }
} }
bool context::is_objective(expr* fml) {
return is_app(fml) && m_objective_fns.contains(to_app(fml)->get_decl());
}
bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) { bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) {
if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) && if (is_app(fml) && m_objective_fns.find(to_app(fml)->get_decl(), index) &&
m_objectives[index].m_type == O_MAXIMIZE) { m_objectives[index].m_type == O_MAXIMIZE) {

1
src/opt/opt_context.h
View file

@ -303,6 +303,7 @@ namespace opt {
void import_scoped_state(); void import_scoped_state();
void normalize(expr_ref_vector const& asms); void normalize(expr_ref_vector const& asms);
void internalize(); void internalize();
bool is_objective(expr* fml);
bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index);
bool is_maxsat(expr* fml, expr_ref_vector& terms, bool is_maxsat(expr* fml, expr_ref_vector& terms,