Clean src/ to remove Unicode (or to mark it as OK)

Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.

make HolQbfLib's sat solver customisable

crude method using a ref cell. if there's a standard better approach let
me know/fix it.

remove calls to Profile.profile in QbfCertificate.sml

presumably only need to run profiling code when testing/improving the
library, not for normal use.

Use CHOOSE+EXISTS instead of INST+PROVE_HYP in HolQbf

This change, suggested by Michael, showed a dramatic speed improvement
(looks like an order of magnitude) on the benchmarks (run by Tjark). It
is not obvious why.

Replace false comment in HolQbf valid certificate checker implementation

Use new Redblackmap update function in HolQbf

Improve HolQbf valid certificate validator

Time complexity should now be O(n*log(n)) where n is the total number of
variables (universal, existential, and extension) in the certificate,
whereas before it was more like O(n*n).

Remove an unused function in QbfCertificate.sml

Slightly improved final sanity checks.

Added functions to prove/decide QBFs. Added profiling calls to QbfCertificate (for now).

QbfCertificate: use alternative method for discharging hypotheses

(To create the theorem for a valid certificate.)
This is hopefully faster than HO_MATCH_MP, although some evidence via
profiling would be nice.

read_qdimacs_file now takes an additional argument, varfn, that translates
QDIMACS variable indices into HOL variable names.

Rewrite of HolQbfLib's valid certificate validator

The new version:
- allows certificates that define extension variables in terms of
other extension variables (which squolem does generate)
- gives the witnesses as equality hypotheses rather than by actual
substitution, to reduce the size of the term passed to SAT_PROVE
- works on almost half of Tjark's tests (not included) in under 60
seconds each

Make dict argument to QbfCertificate.check optional

If SOME dict is passed, it should be a map from variables in the term to
literal indexes. If NONE is passed, assume the term was generated by
QDimacs.read_qdimacs_file, which preserves literal indexes in the
variable names.

Make HolQbfLib prove QBFs (validate Squolem validity certificates)

A sketch that uses SAT_PROVE on a qb formula after replacing the
existential variables with witnesses generated by Squolem.

It works on the simple tautologies in the selftest file.

Parsing of resolution steps more closely follows the grammar in "A File Format
for QBF Certificates".

HolQbfLib now supports Squolem2.

Typo fixed.

Made Moscow ML happy.

Unit tests, tracing, and various other additions.

Tuned.

HolQbfLib: A new library for integrating Quantified Boolean Formulae (QBF)
solvers.

Features so far:

* Translation between (the QBF subset of) HOL and the QDIMACS format
* Checking of Q-resolution based certificates of invalidity, as generated
by the QBF solver Squolem