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

notes on pvar justifications

Browse source
This commit is contained in:
Jakob Rath 2023-07-21 14:55:29 +02:00
parent f14c3c3cb4
commit eb4ea606d5
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/polysat/slicing.cpp
View file

@ -33,6 +33,13 @@ TODO:
- implement query functions
- when solver assigns value of a variable v, add equations with v substituted by its value?
TODO: better conflicts with pvar justification
- pvar justification is only introduced by add_value (when a variable is assigned in the model)
- so there can be at most two pvar justifications in a single conflict
- when explaining a conflict that contains pvars:
- single pvar x: the egraph has derived that x must have a different value c, learn literal x = c (instead of x != value(x) as is done now by the naive integration)
- two pvars x, y: learn literal x = y
*/