v2.6

Functional synthesis and quantifier elimination overhauled again. Now much more simple.

Also fixed a compilation problem with occurring with new GCC versions.

v2.5

New features:

• Certification works now also when CADET uses CEGAR to support its engine (activated by default).
• Functional synthesis and quantifier elimination completely overhauled.
• All certificates, including those from functional synthesis and quantifier elimination are now checked by default, when compiled in debug mode ('./configure --debug').

Changing dependencies:

• Dropped support for Python 2. Now CADET requires Python 3.6+ for its testing scripts.

v2.3.1

Fixed a bug in functional synthesis.

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.

v2.1

This release features cleaned up source code and the new qipasir interface. So far only the non-incremental usage of qipasir is supported.

CADETv2.0

The first public release of the source code of CADET. This is a reimplementation of the version that was used in the paper "Incremental Determinization" that appeared in SAT 2016.

Notable facts:

• With default options, CADET2.0 is performs similar as the original CADET
• No API available as of yet
• User guide available in doc/