mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
#fix #5328
in-processing for "pure" PB constraints isn't model preserving and therefore removed.
This commit is contained in:
parent
85b672ee85
commit
1fd6b66ecc
|
@ -132,7 +132,6 @@ namespace pb {
|
|||
remove_constraint(p, "is tight");
|
||||
}
|
||||
else {
|
||||
|
||||
unsigned sz = p.size();
|
||||
clear_watch(p);
|
||||
unsigned j = 0;
|
||||
|
@ -1470,7 +1469,6 @@ namespace pb {
|
|||
return true;
|
||||
}
|
||||
else if (c.lit() != sat::null_literal && value(c.lit()) != l_true) {
|
||||
// else if (c.lit() != sat::null_literal && value(c.lit()) == l_false) {
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
@ -2025,7 +2023,7 @@ namespace pb {
|
|||
unit_strengthen();
|
||||
cleanup_clauses();
|
||||
cleanup_constraints();
|
||||
update_pure();
|
||||
|
||||
count++;
|
||||
}
|
||||
while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
|
||||
|
@ -2047,41 +2045,6 @@ namespace pb {
|
|||
// if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
|
||||
}
|
||||
|
||||
/*
|
||||
* ~lit does not occur in clauses
|
||||
* ~lit is only in one constraint use list
|
||||
* lit == C
|
||||
* -> ignore assignments to ~lit for C
|
||||
*
|
||||
* ~lit does not occur in clauses
|
||||
* lit is only in one constraint use list
|
||||
* lit == C
|
||||
* -> negate: ~lit == ~C
|
||||
*/
|
||||
void solver::update_pure() {
|
||||
//return;
|
||||
for (constraint* cp : m_constraints) {
|
||||
literal lit = cp->lit();
|
||||
if (lit != sat::null_literal &&
|
||||
!cp->is_pure() &&
|
||||
value(lit) == l_undef &&
|
||||
get_wlist(~lit).size() == 1 &&
|
||||
m_clause_use_list.get(lit).empty()) {
|
||||
clear_watch(*cp);
|
||||
cp->negate();
|
||||
lit.neg();
|
||||
}
|
||||
if (lit != sat::null_literal &&
|
||||
!cp->is_pure() &&
|
||||
m_cnstr_use_list[(~lit).index()].size() == 1 &&
|
||||
get_wlist(lit).size() == 1 &&
|
||||
m_clause_use_list.get(~lit).empty()) {
|
||||
cp->set_pure();
|
||||
get_wlist(~lit).erase(sat::watched(cp->cindex())); // just ignore assignments to false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void solver::mutex_reduction() {
|
||||
literal_vector lits;
|
||||
for (unsigned v = 0; v < s().num_vars(); ++v) {
|
||||
|
|
|
@ -56,6 +56,12 @@ class sat_tactic : public tactic {
|
|||
for (func_decl* f : funs)
|
||||
tout << mk_ismt2_pp(f, m) << "\n";
|
||||
);
|
||||
|
||||
expr_ref_vector fmls_to_validate(m);
|
||||
if (gparams::get_ref().get_bool("model_validate", false))
|
||||
for (unsigned i = 0; i < g->size(); ++i)
|
||||
fmls_to_validate.push_back(g->form(i));
|
||||
|
||||
g->reset();
|
||||
g->m().compact_memory();
|
||||
|
||||
|
@ -65,7 +71,8 @@ class sat_tactic : public tactic {
|
|||
dep2assumptions(dep2asm, assumptions);
|
||||
lbool r = m_solver->check(assumptions.size(), assumptions.data());
|
||||
TRACE("sat", tout << "result of checking: " << r << " ";
|
||||
if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";);
|
||||
if (r == l_undef) tout << m_solver->get_reason_unknown(); tout << "\n";
|
||||
if (m_goal2sat.has_interpreted_funs()) tout << "has interpreted\n";);
|
||||
if (r == l_false) {
|
||||
expr_dependency * lcore = nullptr;
|
||||
if (produce_core) {
|
||||
|
@ -106,6 +113,10 @@ class sat_tactic : public tactic {
|
|||
break;
|
||||
}
|
||||
}
|
||||
for (auto* f : fmls_to_validate)
|
||||
if (md->is_false(f))
|
||||
IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";);
|
||||
|
||||
m_goal2sat.update_model(md);
|
||||
TRACE("sat_tactic", model_v2_pp(tout, *md););
|
||||
g->add(model2model_converter(md.get()));
|
||||
|
|
Loading…
Reference in a new issue