make HolQbfLib's sat solver customisable

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

Renamed decide -> decide_prenex, decide_any -> decide.

Improve HolQbfLib.decide_any

(Progress on #1)

It should now deal with free variables in the input term. Also, fixed a
bug for dealing with a sequence of multiple innermost universal
quantifiers, and in so doing redesigned qbf_prenex_conv substantially.

Also, added another self test and made the self test check for decide_any
check whether an appropriate theorem was produced (rather than assuming
any theorem returned is ok).

Progress on HolQbfLib.decide_any

It should now accept any closed QBF (variables, conjunctions,
disjunctions, implications, quantifiers) as long as all quantified
variables occur somewhere (or maybe even some examples where they
don't).

Improvements to functions in QbfConv welcome.

start attempt to expand HolQbfLib's accepted formula format

remove a bash-ism from HolQbfLib

When /bin/sh is dash (e.g. on Ubuntu I think) HolQbfLib's system call to
squolem2 won't work ("Syntax error: Bad fd number"). This should fix it.

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

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.

HolQbfLib now supports Squolem2.

Unit tests, tracing, and various other additions.