mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Conflict from viable_fallback also depends on the current assignment

Browse source
This commit is contained in:
Jakob Rath 2022-09-23 16:45:56 +02:00
parent 4e4b4fdd06
commit 49590e0e01
1 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polysat/conflict.cpp
View file

@ -251,10 +251,19 @@ namespace polysat {
if (by_viable_fallback) {
logger().begin_conflict(header_with_var("unsat core from viable fallback for v", v));
// Conflict detected by viable fallback:
// initial conflict is the unsat core of the univariate solver
// initial conflict is the unsat core of the univariate solver,
// and the assignment (under which the constraints are univariate in v)
// TODO:
// - currently we add variables directly, which is sound:
// e.g.: v^2 + w^2 == 0; w := 1
// - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
// e.g.: v^2 + w^2 == 0; w^2 == 1
signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
for (auto c : unsat_core)
for (auto c : unsat_core) {
insert(c);
insert_vars(c);
}
SASSERT(!m_vars.contains(v));
// TODO: apply conflict resolution plugins here too?
} else {
logger().begin_conflict(header_with_var("forbidden interval lemma for v", v));