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

unsat core

Browse source
This commit is contained in:
Jakob Rath 2022-03-18 15:49:44 +01:00
parent 509a007ed7
commit fd353bff17
3 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -518,7 +518,7 @@ namespace polysat {
break; break;
case dd::find_t::empty: case dd::find_t::empty:
m_free_pvars.unassign_var_eh(v); m_free_pvars.unassign_var_eh(v);
// TODO: get unsat core from univariate solver auto core = m_viable_fallback.unsat_core(v); // TODO: add constraints from unsat_core to conflict
set_conflict(v); set_conflict(v);
return; return;
} }

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

@ -791,5 +791,14 @@ namespace polysat {
return dd::find_t::empty; return dd::find_t::empty;
} }
} }
signed_constraints viable_fallback::unsat_core(pvar v) {
signed_constraints cs;
for (unsigned dep : m_usolver[v]->unsat_core()) {
cs.push_back(m_constraints[v][dep]);
}
return cs;
}
} }

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

@ -211,7 +211,7 @@ namespace polysat {
// bool check_value(pvar v, rational const& val); // bool check_value(pvar v, rational const& val);
dd::find_t find_viable(pvar v, rational& out_val); dd::find_t find_viable(pvar v, rational& out_val);
// TODO: get unsat core signed_constraints unsat_core(pvar v);
}; };
} }