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