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

disable conflict_var handling for now

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 13:58:41 +02:00
parent c0f51eacf8
commit 2de443c74f
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -229,17 +229,18 @@ namespace polysat {
// NOTE:
// In the "standard" case where "v = val" is on the stack:
// - cjust_v contains true constraints
// - core contains both false and true constraints... (originally only false ones, but additional true ones may come from saturation).
// - core contains both false and true constraints... (originally only false ones, but additional true ones may come from saturation?).
// In the case where no assignment to v is on the stack, i.e., conflict_var == v and viable(v) = \emptyset:
// - the constraints in cjust_v cannot be evaluated.
// - for now, we just pick a value. TODO: revise later
/*
if (conflict_var() == v) {
// Temporary assignment
// (actually we shouldn't just pick any value, but one that makes at least one constraint true...)
LOG_H1("WARNING: temporary assignment of conflict_var");
m_solver->assign_core(v, m_solver->m_value[v], justification::propagation(m_solver->m_level));
}
*/
for (auto c : cjust_v)
insert(c);