On Wed, 2 Jan 2013, Jasmin Blanchette wrote:
Am 01.01.2013 um 22:38 schrieb Makarius:
Anyway, since the "smt" method seems to work right now, I propose to
wire up a test where smt_certificates and smt_read_only_certificates
are left unchanged if ISABELLE_FULL_TEST is enabled. Does that make
sense, according to the meaning of these options? SMT/Z3 should run
without any certificates getting in between.
I gave something like this a try:
Änderung: 50666:6f48853f08d5
Marke: tip
Nutzer: blanchet
Datum: Wed Jan 02 09:31:25 2013 +0100
Zusammenfassung: actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST"
is enabled
The conditionioning of the theories can be done with a little bit of ML
for the options.
What I have right now (without any "ML conditioning") is that
"SMT_Tests" is not run when the full tests are disabled. Then there are
already several other files testing that SMT's certificate mechanism
works. But I won't stop anybody if they want to change the setup so that
"SMT_Tests" runs against certificates in non-full mode.
This looks OK for me. The SMT_Tests are just synthetic, but there are
many of them, and the SMT_Examples don't seem to add so much. "ML
conditioning" would introduce further confusion due to odd variance of the
meaning of theory content.
So we leave it for now. In 935988e2b35a I had already enabled isatest to
work with it, and it seems to have been successful today.
From my side, the SMT/Z3 thread can be closed for the purpose of the
coming release.
If Sasche still wants to make some more refinements, e.g. to address
Z3 proof parser (line 34): unknown function symbol: "S2!val!0"
http://isabelle.in.tum.de/repos/isabelle/annotate/b1f4291eb916/src/HOL/SMT_Examples/SMT_Tests.thy#l122
there are still approx. 2 weeks left to do it.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
