* Closed a loophole in HolSatLib failsafe mechanism.
* Replaced MiniSat's DIMACS parser with my own to avoid
build dependency on zlib, which HolSatLib does
not use. Thanks to Anthony for motivation. Updated
docs.

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.

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.

Upgraded MiniSat to fix GCC 4.1 compile problem. Thanks to Peter Homeier for spotting this.

HolSatLib refactoring and additions.

* MiniSat-p v1.14 added as a "built-in" SAT-solver
* A new function SAT_TAUT_PROVE uses MiniSat to prove propositional
tautologies within HOL
* HolSatLib refactored into satTools and dimacsTools
* Local documentation removed; it was folded into the
Description some time ago.
* The HolSatLib interface remains the same, save for the addition of
SAT_TAUT_PROVE.
* Two minor additions to defCNF: a global ref for the variable name
prefix used by DEF_CNF_VECTOR_CONV (defaulting to the current setting),
and a global ref for the number of new vars introduced by definitional
CNF.