- CDCL
This session the CDCL calculi (Weidenbach and Nieuwenhuis et al.) and the links between
both. It also contains a very simple implementation based on lists and two extensions (restart and
incremental).
This version is based on the Refinement Framework, to make the two-watched-literals part easier to compile
(workaround as long as a session cannot have two parents).
- CDCL_Extensions
This sessions contains the extensions of the CDCL calculus.
- Entailment_Definition
This session contains various (but still general) definition of entailment used
later.
- IsaSAT
We here refine the previous session to generate code.
- More_Refinement_Libs
This session contains some libraries for Refinement.
- More_Sepref
This session contains some libraries for Refinement.
- Normalisation
This session contains the normalisation from general formulas to CNF and DNF.
- Pairing_Heap_LLVM
We here refine the previous session to generate code.
- Watched_Literals
This session contains all theories related to the two-watched literals. It links
the abstract CDCL calculus to a more concrete version with watched literals.
- Weidenbach_Book_Base
This session imports HOL, some additional useful theories from HOL, and our own
extensions above these lemmas.