mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
trying Cezary's example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
56b9c4c8a2
commit
02f74f1028
|
@ -39,6 +39,9 @@ namespace opt {
|
|||
if (m_maxsat_engine == symbol("core_maxsat")) {
|
||||
m_msolver = alloc(core_maxsat, m, s, m_soft_constraints);
|
||||
}
|
||||
else if (m_maxsat_engine == symbol("weighted_maxsat")) {
|
||||
m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights);
|
||||
}
|
||||
else {
|
||||
m_msolver = alloc(fu_malik, m, s, m_soft_constraints);
|
||||
}
|
||||
|
|
|
@ -253,6 +253,7 @@ namespace smt {
|
|||
disj.push_back(m.mk_not(m_min_cost_atom));
|
||||
}
|
||||
if (is_optimal()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(wmaxsat with lower bound: " << weight << "\n";);
|
||||
m_min_cost = weight;
|
||||
m_cost_save.reset();
|
||||
m_cost_save.append(m_costs);
|
||||
|
|
Loading…
Reference in a new issue