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 replay the proof to yield an
Isabelle theorem.
Your application is somewhat different. It seems that you only want to use the
replay functionality of Isabelle. This is not that easy with the structure of
the existing code. Look at src/HOL/Tools/SMT/z3_replay.ML as an entry point to
the replay code. I suggest, however, to formulate your problem as an Isabelle
proof obligation, e.g. a lemma, and apply the “smt” method:
lemma fixes P :: bool assumes P shows P
using assms [[smt_trace]] by smt
The output of the smt method shows the entire interaction with Z3.
Cheers,
Sascha
Von: Johannes Gareis
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
