#
87d21ca1 |
|
14-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get polyscripter to build again (QFRead change) Tutorial build also needs tweaks for remove-term-eqtype
|
#
1a6ffc76 |
|
04-Nov-2007 |
Hasan Amjad <ha227@cam.ac.uk> |
Comments updated to reflect tautLib upgrade.
|
#
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.
|
#
057ad978 |
|
20-Mar-2006 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update dpll example with reference to HolSatLib's SAT_TAUT_PROVE function. (The example in dpll.sml was also not the same as the one in the manual, so fixed this too.)
|
#
1befb451 |
|
20-Aug-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Updated example code to correspond to what is in the Tutorial chapter on proof tool construction.
|
#
4754c34d |
|
08-Aug-2005 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More text describing the DPLL tool. Will update the number about how slow the tautLib version is when it actually get rounds to finishing. Also, source code for what's in the chapter.
|