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.


Von: Johannes Gareis
isabelle-dev mailing list

Reply via email to