mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Simplify revert_decision; disable resolving over new items for now

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 16:21:14 +02:00
parent a4c3a8c640
commit 067902bf31
2 changed files with 8 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/search_state.h
View file

@ -124,7 +124,9 @@ namespace polysat {
} }
bool next() { bool next() {
#if 0 // If you want to resolve over constraints that have been added during conflict resolution, enable this.
try_push_block(); try_push_block();
#endif
if (current > last()) { if (current > last()) {
--current; --current;
return true; return true;

20
src/math/polysat/solver.cpp
View file

@ -453,6 +453,7 @@ namespace polysat {
search_iterator search_it(m_search); search_iterator search_it(m_search);
while (search_it.next()) { while (search_it.next()) {
LOG("search state: " << m_search);
LOG("Conflict: " << m_conflict); LOG("Conflict: " << m_conflict);
auto const& item = *search_it; auto const& item = *search_it;
LOG_H2("Working on " << item); LOG_H2("Working on " << item);
@ -479,7 +480,7 @@ namespace polysat {
sat::bool_var const var = lit.var(); sat::bool_var const var = lit.var();
if (!m_conflict.is_bmarked(var)) if (!m_conflict.is_bmarked(var))
continue; continue;
if (m_bvars.level(var) <= base_level()) if (m_bvars.level(var) <= base_level()) // TODO: this doesn't work with out-of-level-order iteration.
break; break;
if (m_bvars.is_decision(var)) { if (m_bvars.is_decision(var)) {
revert_bool_decision(lit); revert_bool_decision(lit);
@ -600,17 +601,8 @@ namespace polysat {
m_viable.add_non_viable(v, val); m_viable.add_non_viable(v, val);
learn_lemma(v, std::move(lemma)); learn_lemma(v, std::move(lemma));
if (is_conflict()) { if (!is_conflict())
LOG_H1("Conflict during revert_decision/learn_lemma!"); narrow(v);
return;
}
narrow(v);
if (m_justification[v].is_unassigned()) {
m_free_vars.del_var_eh(v);
decide(v);
}
} }
bool solver::is_decision(search_item const& item) const { bool solver::is_decision(search_item const& item) const {
@ -814,8 +806,8 @@ namespace polysat {
for (auto* cl : m_redundant_clauses) { for (auto* cl : m_redundant_clauses) {
out << "\t" << *cl << "\n"; out << "\t" << *cl << "\n";
for (auto lit : *cl) { for (auto lit : *cl) {
auto c = m_constraints.lookup(lit.var()); auto c = m_constraints.lookup(lit);
out << "\t\t" << lit.var() << ": " << *c << "\n"; out << "\t\t" << lit << ": " << c << "\n";
} }
} }
return out; return out;