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

notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-31 09:16:48 -08:00
parent 697b561c7a
commit 486cc632d0
1 changed files with 22 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/math/polysat/conflict.h
View file

@ -36,26 +36,36 @@ Notes:
l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l) l <- ?, < Vars, { l } u C > ===> ~l <- (C & Vars = value(Vars) => ~l)
l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C > l <- asserted, < Vars, { l } u C > ===> < Vars, { l } u C >
l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated l <- Vars', < Vars, { l } u C > ===> < Vars u Vars', C > if all Vars' are propagated
l <- Vars', < Vars, { l } u C > ===> backjump to unassign variable. l <- Vars', < Vars, { l } u C > ===> Mark < Vars, { l } u C > as bailout
v = value <- D, < Vars u { v }, C > ===> < Vars, D u C > v = value <- D, < Vars u { v }, C > ===> < Vars, D u C >
v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value) v = value <- ?, < Vars u { v }, C > ===> v != value <- (C & Vars = value(Vars) => v != value)
Example derivation: Example derivations:
Trail: z <= y <- asserted, Trail: z <= y <- asserted
xz > xy <- asserted, xz > xy <- asserted
x = a <- ?, x = a <- ?
y = b <- ?, y = b <- ?
z = c <- ? z = c <- ?
Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b Conflict: < {x, y, z}, xz > xy > when ~O(a,b) and c <= b
Lemma: x <= a & y <= b => ~O(x,y) Append x <= a <- { x }
Append y <= b <- { y }
Conflict: < {}, y >= z, xz > xy, x <= a, y <= b >
Based on: z <= y & x <= a & y <= b => xz <= xy
Resolve: y <= b <- { y }, y is a decision variable.
Bailout: lemma ~(y >= z & xz > xy & x <= a & y <= b) at decision level of lemma
With overflow predicate:
Append ~O(x, y) <- { x, y } Append ~O(x, y) <- { x, y }
Saturate z <= y & ~O(x,y) => xz <= xy
Conflict: < {}, y >= z, xz > xy, ~O(x,y) > Conflict: < {}, y >= z, xz > xy, ~O(x,y) >
Based on z <= y & ~O(x,y) => xz <= xy
Resolve: ~O(x, y) <- { x, y } both x, y are decision variables
Lemma: y < z or xz <= xy or O(x,y) Lemma: y < z or xz <= xy or O(x,y)
Backjump: "to before y is guessed"
--*/ --*/