v2.3
New features
- Functional synthesis mode with flag "--functional-synthesis". Given a 2QBF "forall X exists Y. phi(X,Y)", the algorithm computes a function that provides a value for Y satisfying phi whenever there exists one.
- Enhanced pure literals: Sketched a stronger version of pure literals; is going to be extended in the future.
Other changes
- Restructured the propagation order
- Restructured some headers for better understandability
- Moved decisions in skolem.c
- Improvement to how constants are handled. Now also deterministic variables can be assigned a constant in hindsight.
- CEGAR autotuning: the algorithm does more CEGAR whenever it turns out to produce small clauses.
- Introduced new example domain, that propagates examples of universal assignments. Warning: Not yet working correctly.