mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

finish explanation code for viable

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-26 14:17:24 -08:00
parent 6466345755
commit 9cce1ff836
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/polysat/viable.cpp
View file

@ -520,12 +520,19 @@ namespace polysat {
}
/*
* Explain why the current variable is not viable or signleton.
* Explain why the current variable is not viable or
* or why it can only have a single value.
*/
dependency_vector viable::explain() {
dependency_vector result;
uint_set seen;
for (auto e : m_explain) {
auto index = e->constraint_index;
if (seen.contains(index))
continue;
if (m_var != e->var)
result.push_back(offset_claim(m_var, {e->var, 0}));
seen.insert(index);
auto const& [sc, d, value] = c.m_constraint_index[index];
result.push_back(d);
result.append(c.explain_eval(sc));