mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
update pd-maxres
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
0bc45ca250
commit
e4ce6b6d74
2 changed files with 48 additions and 36 deletions
|
|
@ -41,6 +41,7 @@ namespace sat {
|
|||
m_mus.append(m_core);
|
||||
s.m_core.reset();
|
||||
s.m_core.append(m_mus);
|
||||
TRACE("sat", tout << "new core: " << s.m_core << "\n";);
|
||||
}
|
||||
|
||||
void mus::update_model() {
|
||||
|
|
@ -61,7 +62,7 @@ namespace sat {
|
|||
flet<bool> _disable_min_partial(s.m_config.m_minimize_core_partial, false);
|
||||
flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
|
||||
flet<bool> _is_active(m_is_active, true);
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
|
||||
reset();
|
||||
return mus1();
|
||||
}
|
||||
|
|
@ -77,7 +78,7 @@ namespace sat {
|
|||
unsigned delta_time = 0;
|
||||
unsigned core_miss = 0;
|
||||
while (!core.empty()) {
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "(opt.mus reducing core: " << core.size() << " mus: " << mus.size() << ")\n";);
|
||||
TRACE("sat",
|
||||
tout << "core: " << core << "\n";
|
||||
tout << "mus: " << mus << "\n";);
|
||||
|
|
@ -121,12 +122,12 @@ namespace sat {
|
|||
case l_false:
|
||||
literal_vector const& new_core = s.get_core();
|
||||
if (new_core.contains(~lit)) {
|
||||
IF_VERBOSE(2, verbose_stream() << "miss core " << lit << "\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "miss core " << lit << "\n";);
|
||||
++core_miss;
|
||||
}
|
||||
else {
|
||||
core_miss = 0;
|
||||
TRACE("sat", tout << "new core: " << new_core << "\n";);
|
||||
TRACE("sat", tout << "core: " << new_core << " mus: " << mus << "\n";);
|
||||
core.reset();
|
||||
for (unsigned i = 0; i < new_core.size(); ++i) {
|
||||
literal lit = new_core[i];
|
||||
|
|
@ -146,9 +147,8 @@ namespace sat {
|
|||
delta_time = 0;
|
||||
}
|
||||
}
|
||||
TRACE("sat", tout << "new core: " << mus << "\n";);
|
||||
set_core();
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";);
|
||||
return l_true;
|
||||
}
|
||||
|
||||
|
|
@ -160,7 +160,7 @@ namespace sat {
|
|||
lbool is_sat = qx(core, support, false);
|
||||
s.m_core.reset();
|
||||
s.m_core.append(core.to_vector());
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "(sat.mus.new " << s.m_core << ")\n";);
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
|
@ -269,11 +269,11 @@ namespace sat {
|
|||
if (is_sat == l_true) {
|
||||
m_mus.push_back(tabu[i]);
|
||||
m_core.erase(tabu[i]);
|
||||
IF_VERBOSE(2, verbose_stream() << "in core " << tabu[i] << "\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "in core " << tabu[i] << "\n";);
|
||||
reuse_model = true;
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(2, verbose_stream() << "NOT in core " << tabu[i] << "\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "NOT in core " << tabu[i] << "\n";);
|
||||
reuse_model = false;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -943,23 +943,25 @@ namespace sat {
|
|||
flet<bool> _min2(m_config.m_minimize_core_partial, false);
|
||||
m_weight = 0;
|
||||
m_blocker.reset();
|
||||
m_min_core_valid = false;
|
||||
m_min_core.reset();
|
||||
svector<lbool> values;
|
||||
unsigned num_cores = 0;
|
||||
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
|
||||
literal lit = lits[i];
|
||||
SASSERT(is_external(lit.var()));
|
||||
TRACE("sat", tout << "propagate: " << lit << " " << value(lit) << "\n";);
|
||||
SASSERT(m_scope_lvl == 1);
|
||||
|
||||
add_assumption(lit);
|
||||
switch(value(lit)) {
|
||||
case l_undef:
|
||||
add_assumption(lit);
|
||||
values.push_back(l_true);
|
||||
assign(lit, justification());
|
||||
propagate(false);
|
||||
if (num_cores*2 >= num_lits) {
|
||||
break;
|
||||
}
|
||||
propagate(false);
|
||||
if (inconsistent()) {
|
||||
pop_assumption();
|
||||
flet<bool> _init(m_initializing_preferred, true);
|
||||
while (inconsistent()) {
|
||||
while (inconsistent()) {
|
||||
if (!resolve_conflict()) {
|
||||
return true;
|
||||
}
|
||||
|
|
@ -968,23 +970,33 @@ namespace sat {
|
|||
if (m_scope_lvl == 0) {
|
||||
return false;
|
||||
}
|
||||
for (; i < num_lits; ++i) {
|
||||
literal lit = lits[i];
|
||||
if (value(lit) == l_undef) {
|
||||
assign(lit, justification());
|
||||
add_assumption(lit);
|
||||
// backjump to last consistent assumption:
|
||||
unsigned j;
|
||||
for (j = 0; j < i && value(lits[j]) == values[j]; ++j);
|
||||
SASSERT(value(lits[j]) != values[j]);
|
||||
SASSERT(j <= i);
|
||||
SASSERT(j == 0 || value(lits[j-1]) == values[j-1]);
|
||||
for (unsigned k = i; k >= j; --k) {
|
||||
if (is_assumption(lits[k])) {
|
||||
pop_assumption();
|
||||
}
|
||||
}
|
||||
return true;
|
||||
values.resize(j);
|
||||
TRACE("sat", tout << "backjump " << (i - j + 1) << " steps " << num_cores << "\n";);
|
||||
i = j - 1;
|
||||
}
|
||||
break;
|
||||
|
||||
case l_false:
|
||||
add_assumption(lit);
|
||||
++num_cores;
|
||||
values.push_back(l_false);
|
||||
SASSERT(!inconsistent());
|
||||
set_conflict(justification(), ~lit);
|
||||
m_conflict_lvl = m_scope_lvl;
|
||||
m_conflict_lvl = scope_lvl();
|
||||
resolve_conflict_for_unsat_core();
|
||||
IF_VERBOSE(3, verbose_stream() << "core: " << m_core << "\n";);
|
||||
update_min_core();
|
||||
SASSERT(m_min_core_valid);
|
||||
m_weight += weights[i];
|
||||
if (m_weight <= max_weight) {
|
||||
m_blocker.push_back(lit);
|
||||
|
|
@ -998,26 +1010,18 @@ namespace sat {
|
|||
IF_VERBOSE(11, verbose_stream() << "small core: " << m_core << "\n";);
|
||||
return true;
|
||||
}
|
||||
update_min_core();
|
||||
SASSERT(m_min_core_valid);
|
||||
pop_assumption();
|
||||
m_inconsistent = false;
|
||||
break;
|
||||
case l_true: {
|
||||
justification j = m_justification[lit.var()];
|
||||
if (j.get_kind() == justification::NONE) {
|
||||
add_assumption(lit);
|
||||
}
|
||||
case l_true:
|
||||
values.push_back(l_true);
|
||||
SASSERT(m_justification[lit.var()].get_kind() != justification::NONE || lvl(lit) == 0);
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("sat", tout << "initialized\n";);
|
||||
IF_VERBOSE(11, verbose_stream() << "Blocker: " << m_blocker << "\nCore: " << m_min_core << "\n";);
|
||||
if (m_min_core_valid && m_blocker.size() >= m_min_core.size()) {
|
||||
reassert_min_core();
|
||||
}
|
||||
else if (m_weight >= max_weight) {
|
||||
if (m_weight >= max_weight) {
|
||||
// block the current correction set candidate.
|
||||
++m_stats.m_blocked_corr_sets;
|
||||
TRACE("opt", tout << "blocking soft correction set: " << m_blocker << "\n";);
|
||||
|
|
@ -1103,6 +1107,8 @@ namespace sat {
|
|||
m_stopwatch.reset();
|
||||
m_stopwatch.start();
|
||||
m_core.reset();
|
||||
m_min_core_valid = false;
|
||||
m_min_core.reset();
|
||||
TRACE("sat", display(tout););
|
||||
|
||||
if (m_config.m_bcd) {
|
||||
|
|
@ -2005,11 +2011,17 @@ namespace sat {
|
|||
}
|
||||
reset_unmark(old_size);
|
||||
if (m_config.m_minimize_core || m_config.m_minimize_core_partial) {
|
||||
if (m_min_core_valid && m_min_core.size() < m_core.size()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
|
||||
m_core.reset();
|
||||
m_core.append(m_min_core);
|
||||
}
|
||||
// TBD:
|
||||
// apply optional clause minimization by detecting subsumed literals.
|
||||
// initial experiment suggests it has no effect.
|
||||
m_mus(); // ignore return value on cancelation.
|
||||
set_model(m_mus.get_model());
|
||||
IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue