#
97b7d190 |
|
03-Dec-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Reformat to remove lines longer than 80 columns in src/HolSat
|
#
6a81a039 |
|
21-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove TABs from src Will also make selftest to check that they aren't introduced
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
e07db070 |
|
08-Aug-2007 |
Hasan Amjad <ha227@cam.ac.uk> |
Summary: tautLib upgraded to use HolSatLib engine. Details: * tautLib signature (and behaviour hopefully!) is unchanged. Internally, TAUT_CHECK_CONV now uses HolSatLib. * HolSatLib can now handle Boolean-valued conditionals. This was forced because tautLib handled them. * We now have full drop-in support for zChaff, via a proof translator. * HolSatLib now deletes temporary files. * Legacy HolSatLib interface dropped in favour of simpler interface with single entry-point, plus some convenience wrappers. * examples/miller/m renamed to selftest.exe; now works with build -selftest * build-sequence changes: src/compute and src/HolSat/* moved above src/taut; examples/miller stuff condensed into one entry * build.sml patched to handle zChaff proof translator (in C++). * New windows binaries for MiniSat and zChaff proof translator. * Changes/additions to HolSatLib interface rippled to affected files. * Documentation updated. In particular, HolSatLib section in Description had to be almost completely rewritten. * HOL builds to selftest level 1 on standard kernel, and level 2 on experimental kernel. Level 2 failures on standard are non-critical and authors have been informed.
|
#
d8cf5be0 |
|
30-Oct-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
* Implicit definitional CNF (from HOL Light code due to John Harrison), modified to exploit primitive CONJUNCT* rules in HOL4. * Optimisations to above for the case where problem is already CNF. This is handy for SATLIB problems. * Fallback to SML DPLL prover extended to the case where MiniSat binary cannot be found or cannot be executed. * SML DPLL prover modified to use implicit def CNF, and to produce countermodels in the same format as SAT_TAUT_PROVE. * Explicit definitional CNF and normalFormsTest files removed, so we can move HolSatLib up the build-sequence, to follow src/taut.
|
#
0c840916 |
|
29-Sep-2006 |
Hasan Amjad <ha227@cam.ac.uk> |
Some technical improvements: * HOL-side - All is now tail recursive and most uses less RAM - Undocumented feature allows skipping CNF conversion (still WIP) - General refactoring preparatory to adding proof replay for ZChaff * Solver-side - Proof log now indexes root clauses, and writes sign info for pivots - Proof::compress has been implemented - Folded in miscellaneous upstream deltas PS: None of the above applies to defCNF stuff. Still a black box to me.
|