mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

some fixes

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 15:46:50 +02:00
parent ff1185891a
commit 40d62af796
2 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/math/polysat/conflict_core.cpp
View file

@ -129,7 +129,7 @@ namespace polysat {
// (we still need the list though, for new/temporary constraints.)
int j = 0;
for (auto c : m_constraints)
if (c->bvar() == var)
if (c->bvar() != var)
m_constraints[j++] = c;
m_constraints.shrink(j);
@ -189,7 +189,9 @@ namespace polysat {
}
clause_builder conflict_core::build_core_lemma(unsigned model_level) {
LOG_H3("build lemma from core");
LOG_H3("Build lemma from core");
LOG("core: " << *this);
LOG("model_level: " << model_level);
clause_builder lemma(*m_solver);
// TODO: try a final core reduction step?
@ -197,7 +199,7 @@ namespace polysat {
for (auto c : m_constraints) {
if (!c->has_bvar())
keep(c);
lemma.push(c);
lemma.push(~c);
}
if (m_needs_model) {
@ -210,6 +212,8 @@ namespace polysat {
// Add v != val for each variable
for (pvar v : vars) {
// SASSERT(!m_solver->m_justification[v].is_unassigned()); // TODO: why does this trigger????
if (m_solver->m_justification[v].is_unassigned())
continue;
if (m_solver->m_justification[v].level() > model_level)
continue;
auto diseq = ~cm().eq(lemma.level(), m_solver->var(v) - m_solver->m_value[v]);
@ -225,7 +229,7 @@ namespace polysat {
if (is_bailout())
return build_fallback_lemma(reverted_level);
else
return build_core_lemma(reverted_level - 1);
return build_core_lemma(reverted_level);
}
bool conflict_core::resolve_value(pvar v, vector<signed_constraint> const& cjust_v) {

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

@ -590,7 +590,6 @@ namespace polysat {
LOG_H3("Guessing literal in lemma: " << lemma);
IF_LOGGING(m_viable.log());
LOG("Boolean assignment: " << m_bvars);
SASSERT(lemma.size() >= 2);
// To make a guess, we need to find an unassigned literal that is not false in the current model.
auto is_suitable = [this](sat::literal lit) -> bool {
@ -940,18 +939,25 @@ namespace polysat {
signed_constraints cs;
cs.append(m_original.size(), m_original.data());
cs.append(m_redundant.size(), m_redundant.data());
// Skip boolean literals that aren't active yet
uint_set skip;
for (unsigned i = m_qhead; i < m_search.size(); ++i)
if (m_search[i].is_boolean())
skip.insert(m_search[i].lit().to_uint());
for (auto c : cs) {
SASSERT(c->has_bvar());
if (skip.contains(c.blit().to_uint()))
continue;
int64_t num_watches = 0;
for (auto const& wlist : m_watch) {
auto n = std::count(wlist.begin(), wlist.end(), c);
VERIFY(n <= 1); // no duplicates in the watchlist
num_watches += n;
}
switch (c->vars().size()) {
case 0: VERIFY(num_watches == 0); break;
case 1: VERIFY(num_watches == 1); break;
default: VERIFY(num_watches == 2); break;
}
unsigned expected_watches = std::min(2u, c->vars().size());
if (num_watches != expected_watches)
LOG("wrong number of watches: " << c);
SASSERT_EQ(num_watches, expected_watches);
}
return true;
}