Quoting Lars Noschinski <nosch...@in.tum.de>:
On 04.06.2012 09:28, Sascha Boehme wrote:
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option "z3_with_extensions". Minor
INCOMPATIBILITY.
What is the reasoning behind this change?
Z3 is mostly used as backend of Sledgehammer these days. Experiments
with Sledgehammer indicate that Z3 is capable of solving problems of
nonlinear arithmetic when multiplication is treated uninterpreted and
when given enough suitable facts. That is, such an approach increases
Sledgehammer's overall success rate. However, when resting on the
interpreted multiplication of Z3, proof reconstruction fails in
several cases resulting in lost proofs -- something which I consider
annoying for users. And instead of letting Sledgehammer emit the line
using [[z3_with_extensions=false]] by (smt fact1 ... factn)
I decided to disable Z3's support for nonlinear arithmetic (and other
features) by default. Note that you can always recover the original
behavior by adding this line at the top of your theory:
declare [[z3_with_extensions]]
Cheers,
Sascha
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
