Jasmin Blanchette wrote:
This motivates me to attack the "linarith" problem. If nobody
objects, I'll call the property "linarith_verbose" and have it on by
default (for compatibility) but off in "try_methods" and "try". I've
also taken the liberty to reword the "counterexample trace" message
Quoting Alexander Krauss :
However, some components do not come with the release (vampire,
yices, jedit_build). Should we simply have a directory at TUM which
is served via http and where developers can get components? Maybe
simply serve /home/isabelle/contrib_devel for that (For jedit_build
thi
> What is the status of remote_z3?
You’re right. It was necessary years ago when only a Windows version of Z3 was
available. Fortunately, the situation has changed meanwhile.
Unless Sledgehammer requires the remote_z3 service, any references to this
obsolete service can now be removed from
* New internal SAT solver "dpll_p" that produces models and proof traces.
This refers to Isabelle/848d507584db. The added SAT solver should be more
efficient than the internal SAT solvers "dpll" and "enumerate". Since the
solver "dpll_p" produces proof traces, the tactics sat and satx can be
Hi Johannes,
Note that emails are typically written in English on this mailing list.
Isabelle uses Z3 to find proofs for goals that are formulated by users. The
query to Z3 is generated by Isabelle. The UNSAT answer from Z3, i.e., the proof
trace, is parsed by Isabelle, which then tries to repl
