1(* Copyright (c) 2009-2010 Tjark Weber. All rights reserved. *)
2
3(* Proof reconstruction for Z3: SML type of Z3 proofs *)
4
5structure Z3_Proof =
6struct
7
8  (* A single Z3 inference step is represented as a value of type
9     'proofterm'.  This datatype has one constructor for each
10     inference rule of Z3.  Premises of the inference step are given
11     by proofterms.  However, to allow encoding of a proof as a graph
12     (rather than a tree), there is an 'ID' constructor that merely
13     takes an integer argument (which is an index into the 'proof'
14     dictionary, cf. type 'proof' below).  The inference step's
15     conclusion is given as a term.  Additionally, there is a
16     'THEOREM' constructor that encapsulates the theorem that is
17     obtained from replaying the inference step in HOL. *)
18
19  (* At the time of writing (2010-09-08), the Z3 documentation
20     unfortunately is outdated with respect to the inference rules
21     that the most recent Z3 version (2.11) uses.  I have applied Z3
22     to a large number of SMT-LIB benchmarks.  'proofterm' provides a
23     constructor for each inference rule that appears (at least once)
24     in the generated proofs.  Rules that only appear in compressed Z3
25     proofs (PROOF_MODE=1) are NOT supported.
26
27     To add another inference rule, one must 1. add a corresponding
28     'proofterm' datatype constructor below; 2. modify
29     Z3_ProofParser.sml so that the parser recognizes the new rule's
30     concrete syntax; 3. modify Z3_ProofReplay.sml so that
31     'check_proof' knows how to validate inferences performed by the
32     new rule. *)
33
34  datatype proofterm = AND_ELIM of proofterm * Term.term
35                     | ASSERTED of Term.term
36                     | COMMUTATIVITY of Term.term
37                     | DEF_AXIOM of Term.term
38                     | ELIM_UNUSED of Term.term
39                     | HYPOTHESIS of Term.term
40                     | IFF_TRUE of proofterm * Term.term
41                     | LEMMA of proofterm * Term.term
42                     | MONOTONICITY of proofterm list * Term.term
43                     | MP of proofterm * proofterm * Term.term
44                     | NOT_OR_ELIM of proofterm * Term.term
45                     | QUANT_INTRO of proofterm * Term.term
46                     | REWRITE of Term.term
47                     | SYMM of proofterm * Term.term
48                     | TH_LEMMA_ARITH of proofterm list * Term.term
49                     | TH_LEMMA_ARRAY of proofterm list * Term.term
50                     | TH_LEMMA_BASIC of proofterm list * Term.term
51                     | TH_LEMMA_BV of proofterm list * Term.term
52                     | TRANS of proofterm * proofterm * Term.term
53                     | TRUE_AXIOM of Term.term
54                     | UNIT_RESOLUTION of proofterm list * Term.term
55                     | ID of int
56                     | THEOREM of Thm.thm
57
58  (* The Z3 proof is a directed acyclic graph of inference steps.  A
59     unique integer ID is assigned to each inference step.  Note that
60     Z3 assigns no ID to the proof's root node, which derives the
61     final theorem "... |- F".  We will use ID 0 for the root node. *)
62
63  type proof = (int, proofterm) Redblackmap.dict
64
65end
66