mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
revising pd-maxres
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
76c9abada2
commit
ee458fa601
|
@ -247,6 +247,7 @@ public:
|
|||
break;
|
||||
}
|
||||
}
|
||||
m_lower = m_upper;
|
||||
trace();
|
||||
return l_true;
|
||||
}
|
||||
|
@ -468,6 +469,9 @@ public:
|
|||
fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr()));
|
||||
s().assert_expr(fml);
|
||||
m_lower += w;
|
||||
if (m_st == s_primal_dual) {
|
||||
m_lower = std::min(m_lower, m_upper);
|
||||
}
|
||||
trace();
|
||||
}
|
||||
|
||||
|
|
|
@ -959,11 +959,13 @@ namespace sat {
|
|||
assign(lit, justification());
|
||||
break;
|
||||
case l_false: {
|
||||
m_assumptions.push_back(lit);
|
||||
SASSERT(!inconsistent());
|
||||
set_conflict(justification(), ~lit);
|
||||
flet<bool> _min1(m_config.m_minimize_core, false);
|
||||
flet<bool> _min2(m_config.m_minimize_core_partial, false);
|
||||
resolve_conflict_for_unsat_core();
|
||||
m_assumptions.pop_back();
|
||||
weight += weights[i];
|
||||
blocker.push_back(lit);
|
||||
TRACE("sat", tout << "core: " << m_core << "\nassumptions: " << m_assumptions << "\n";);
|
||||
|
|
Loading…
Reference in a new issue