mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

use only maxres if there is a lexicographic objective, fix #6697

Browse source 
- maxlex.enable heuristic does not work if it is chained among multiple objectives. Only maxres is set up to commit the proper constraints.
This commit is contained in:
Nikolaj Bjorner 2023-04-24 20:20:26 -07:00
parent 7a689c3298
commit fdd5c923ed
3 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/opt/maxsmt.cpp
View file

@ -178,14 +178,14 @@ namespace opt {
maxsmt::maxsmt(maxsat_context& c, unsigned index): maxsmt::maxsmt(maxsat_context& c, unsigned index):
m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {} m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {}
lbool maxsmt::operator()() { lbool maxsmt::operator()(bool committed) {
lbool is_sat = l_undef; lbool is_sat = l_undef;
m_msolver = nullptr; m_msolver = nullptr;
opt_params optp(m_params); opt_params optp(m_params);
symbol const& maxsat_engine = m_c.maxsat_engine(); symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
if (optp.maxlex_enable() && is_maxlex(m_soft)) if (!committed && optp.maxlex_enable() && is_maxlex(m_soft))
m_msolver = mk_maxlex(m_c, m_index, m_soft); m_msolver = mk_maxlex(m_c, m_index, m_soft);
else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null)
m_msolver = mk_maxres(m_c, m_index, m_soft); m_msolver = mk_maxres(m_c, m_index, m_soft);
@ -401,7 +401,7 @@ namespace opt {
for (auto const& p : soft) { for (auto const& p : soft) {
maxsmt.add(p.first, p.second); maxsmt.add(p.first, p.second);
} }
lbool r = maxsmt(); lbool r = maxsmt(true);
if (r == l_true) { if (r == l_true) {
svector<symbol> labels; svector<symbol> labels;
maxsmt.get_model(m_model, labels); maxsmt.get_model(m_model, labels);

2
src/opt/maxsmt.h
View file

@ -137,7 +137,7 @@ namespace opt {
params_ref m_params; params_ref m_params;
public: public:
maxsmt(maxsat_context& c, unsigned id); maxsmt(maxsat_context& c, unsigned id);
lbool operator()(); lbool operator()(bool committed);
void updt_params(params_ref& p); void updt_params(params_ref& p);
void add(expr* f, rational const& w); void add(expr* f, rational const& w);
unsigned size() const { return m_soft.size(); } unsigned size() const { return m_soft.size(); }

4
src/opt/opt_context.cpp
View file

@ -453,8 +453,8 @@ namespace opt {
lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) { lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) {
model_ref tmp; model_ref tmp;
maxsmt& ms = *m_maxsmts.find(id); maxsmt& ms = *m_maxsmts.find(id);
if (scoped) get_solver().push(); if (scoped) get_solver().push();
lbool result = ms(); lbool result = ms(committed);
if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) { if (result != l_false && (ms.get_model(tmp, m_labels), tmp.get())) {
ms.get_model(m_model, m_labels); ms.get_model(m_model, m_labels);
} }