mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

assign conflict_var

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 09:25:14 +02:00
parent c7129d2537
commit 3f15bf5963
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -214,7 +214,14 @@ namespace polysat {
// - 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: // 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. // - the constraints in cjust_v cannot be evaluated.
// - TODO: what to do here? pick some value? // - 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) for (auto c : cjust_v)
insert(c); insert(c);