#
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.
|