Email Gateway (Mar 05 2021 at 12:29): Email Gateway (Mar 05 2021 at 12:29):From: Thomas Sewell <tals4@cam.ac.uk>
Hi Isabelle users.
I've been doing some proofs in Isabelle about operations of a CPU
architecture lately[1]. Sometimes this just requires bit-blasting, i.e.
reduction of a word/bitvector problem to a boolean problem for
sat-solving.
I've got some satisfactory results using an adjusted version of the old
Word_Bitwise and the Argo prover. I don't think there's currently a
better
approach in Isabelle, since replay of SMT word/bitvector proofs was
never
enabled. (Please tell me if I'm misinformed, I don't seem to be up to
date
about any of this, and there's a note about veriT and a session
HOL-Word-SMT_Examples in the Isabelle 2021 NEWS that I don't
understand.)
I'll try to make an adjusted/improved Word_Bitwise available in the
future, but my version is still quite experimental.
I have been pleasantly surprised how effective Argo was for SAT-like
problems.
Given that, I'd like to make some suggestions, mostly about
documentation.
I think that some kind of note should be added to the SAT theory, or the
sat/satx methods and tactics, given that most users should just call
argo
directly. SAT is the logical place to look for a solver for sat-like
problems,
and the provided default SAT/CDCL solver used by the sat/satx methods is
just not as good as the equivalent implemented within argo. Meanwhile
there's
and unsolved problem with explosion of the problem size in satx
preprocessing.
In principle an external solver might have power that an inbuilt one
doesn't,
but my quick investigation suggests that most of the supported external
SAT
solvers are obscure or historical.
Another minor documentation complaint is that Argo is pretty well
documented in
HOL/ex/Argo_Examples.thy, but it took me a while to think to look there.
In
particular, for medium-size SAT problems a user may have to increase
argo_timeout,
and it's not necessarily obvious where to find it. Perhaps a link to the
examples
in Argo.thy itself?
Finally, some practical issues. While argo generally performs well, in
some
situations I've seen a big difference between the speed of "apply
(argo)" and
"apply (intro impI; argo)". Note that I don't want to just apply
clarsimp or
similar here for various performance reasons, which is probably unusual.
Anyway I don't really understand why an SMT/SAT tool would perform so
differently
for obviously similar goals. I've also discovered what is probably an
outright bug.
A particular kind of trivial premise seems to lead to ML exceptions of
the form
"Undeclared hyps: ..." or "forall_intr: variable .. free in
assumptions". I think
the second might be side-effect of the first. Again, simplification
prevents this
issue, but I have performance reasons to prefer to use the simplifier as
little as
possible.
I've checked these issues still exists in Isabelle 2021, and I attach a
theory which
demonstrates them. Are there any experts who might be interested in
helping me debug
these?
Cheers,
Thomas.
Email Gateway (May 16 2021 at 13:55):From: Makarius <makarius@sketis.net>
This rather old threads appears to be still open. It also looks like
attachments were missing.
Makarius
Email Gateway (May 18 2021 at 13:43):From: Thomas Sewell <tals4@cam.ac.uk>
Indeed. I attach the missing example theory, given that I bothered to
generate it. Given that nobody else has replied, it's perhaps unlikely
at this point that anyone is interested in investigating.
In the meanwhile, I've been taking another approach, and there are
workarounds anyway, so it's unlikely that I'll be doing much
investigating
of possible improvements/fixes myself.
Thanks for following up,
Thomas.
Argo_Issues.thy
Last updated: Jul 15 2022 at 23:21 UTC