1(* Title: HOL/Tools/SMT/z3_proof.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Z3 proofs: parsing and abstract syntax tree. 5*) 6 7signature Z3_PROOF = 8sig 9 (*proof rules*) 10 datatype z3_rule = 11 True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | Symmetry | Transitivity | 12 Transitivity_Star | Monotonicity | Quant_Intro | Distributivity | And_Elim | Not_Or_Elim | 13 Rewrite | Rewrite_Star | Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | 14 Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False | 15 Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | 16 Cnf_Star | Skolemize | Modus_Ponens_Oeq | Th_Lemma of string 17 18 val is_assumption: z3_rule -> bool 19 val string_of_rule: z3_rule -> string 20 21 (*proofs*) 22 datatype z3_step = Z3_Step of { 23 id: int, 24 rule: z3_rule, 25 prems: int list, 26 concl: term, 27 fixes: string list, 28 is_fix_step: bool} 29 30 (*proof parser*) 31 val parse: typ Symtab.table -> term Symtab.table -> string list -> 32 Proof.context -> z3_step list * Proof.context 33end; 34 35structure Z3_Proof: Z3_PROOF = 36struct 37 38open SMTLIB_Proof 39 40 41(* proof rules *) 42 43datatype z3_rule = 44 True_Axiom | Asserted | Goal | Modus_Ponens | Reflexivity | Symmetry | Transitivity | 45 Transitivity_Star | Monotonicity | Quant_Intro | Distributivity | And_Elim | Not_Or_Elim | 46 Rewrite | Rewrite_Star | Pull_Quant | Pull_Quant_Star | Push_Quant | Elim_Unused_Vars | 47 Dest_Eq_Res | Quant_Inst | Hypothesis | Lemma | Unit_Resolution | Iff_True | Iff_False | 48 Commutativity | Def_Axiom | Intro_Def | Apply_Def | Iff_Oeq | Nnf_Pos | Nnf_Neg | Nnf_Star | 49 Cnf_Star | Skolemize | Modus_Ponens_Oeq | Th_Lemma of string 50 (* some proof rules include further information that is currently dropped by the parser *) 51 52val rule_names = Symtab.make [ 53 ("true-axiom", True_Axiom), 54 ("asserted", Asserted), 55 ("goal", Goal), 56 ("mp", Modus_Ponens), 57 ("refl", Reflexivity), 58 ("symm", Symmetry), 59 ("trans", Transitivity), 60 ("trans*", Transitivity_Star), 61 ("monotonicity", Monotonicity), 62 ("quant-intro", Quant_Intro), 63 ("distributivity", Distributivity), 64 ("and-elim", And_Elim), 65 ("not-or-elim", Not_Or_Elim), 66 ("rewrite", Rewrite), 67 ("rewrite*", Rewrite_Star), 68 ("pull-quant", Pull_Quant), 69 ("pull-quant*", Pull_Quant_Star), 70 ("push-quant", Push_Quant), 71 ("elim-unused", Elim_Unused_Vars), 72 ("der", Dest_Eq_Res), 73 ("quant-inst", Quant_Inst), 74 ("hypothesis", Hypothesis), 75 ("lemma", Lemma), 76 ("unit-resolution", Unit_Resolution), 77 ("iff-true", Iff_True), 78 ("iff-false", Iff_False), 79 ("commutativity", Commutativity), 80 ("def-axiom", Def_Axiom), 81 ("intro-def", Intro_Def), 82 ("apply-def", Apply_Def), 83 ("iff~", Iff_Oeq), 84 ("nnf-pos", Nnf_Pos), 85 ("nnf-neg", Nnf_Neg), 86 ("nnf*", Nnf_Star), 87 ("cnf*", Cnf_Star), 88 ("sk", Skolemize), 89 ("mp~", Modus_Ponens_Oeq)] 90 91fun is_assumption Asserted = true 92 | is_assumption Goal = true 93 | is_assumption Hypothesis = true 94 | is_assumption Intro_Def = true 95 | is_assumption Skolemize = true 96 | is_assumption _ = false 97 98fun rule_of_string name = 99 (case Symtab.lookup rule_names name of 100 SOME rule => rule 101 | NONE => error ("unknown Z3 proof rule " ^ quote name)) 102 103fun string_of_rule (Th_Lemma kind) = "th-lemma" ^ (if kind = "" then "" else " " ^ kind) 104 | string_of_rule r = 105 let fun eq_rule (s, r') = if r = r' then SOME s else NONE 106 in the (Symtab.get_first eq_rule rule_names) end 107 108 109(* proofs *) 110 111datatype z3_node = Z3_Node of { 112 id: int, 113 rule: z3_rule, 114 prems: z3_node list, 115 concl: term, 116 bounds: string list} 117 118fun mk_node id rule prems concl bounds = 119 Z3_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} 120 121fun string_of_node ctxt = 122 let 123 fun str depth (Z3_Node {id, rule, prems, concl, bounds}) = 124 replicate_string depth " " ^ 125 enclose "{" "}" (commas 126 [string_of_int id, 127 string_of_rule rule, 128 enclose "[" "]" (space_implode " " bounds), 129 Syntax.string_of_term ctxt concl] ^ 130 cat_lines (map (prefix "\n" o str (depth + 1)) prems)) 131 in str 0 end 132 133datatype z3_step = Z3_Step of { 134 id: int, 135 rule: z3_rule, 136 prems: int list, 137 concl: term, 138 fixes: string list, 139 is_fix_step: bool} 140 141fun mk_step id rule prems concl fixes is_fix_step = 142 Z3_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes, 143 is_fix_step = is_fix_step} 144 145 146(* proof parser *) 147 148fun rule_of (SMTLIB.Sym name) = rule_of_string name 149 | rule_of (SMTLIB.S (SMTLIB.Sym "_" :: SMTLIB.Sym name :: args)) = 150 (case (name, args) of 151 ("th-lemma", SMTLIB.Sym kind :: _) => Th_Lemma kind 152 | _ => rule_of_string name) 153 | rule_of r = raise SMTLIB_PARSE ("bad Z3 proof rule format", r) 154 155fun node_of p cx = 156 (case p of 157 SMTLIB.Sym name => 158 (case lookup_binding cx name of 159 Proof node => (node, cx) 160 | Tree p' => 161 cx 162 |> node_of p' 163 |-> (fn node => pair node o update_binding (name, Proof node)) 164 | _ => raise SMTLIB_PARSE ("bad Z3 proof format", p)) 165 | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, p] => 166 with_bindings (map dest_binding bindings) (node_of p) cx 167 | SMTLIB.S (name :: parts) => 168 let 169 val (ps, p) = split_last parts 170 val r = rule_of name 171 in 172 cx 173 |> fold_map node_of ps 174 ||>> `(with_fresh_names (term_of p)) 175 ||>> next_id 176 |>> (fn ((prems, (t, ns)), id) => mk_node id r prems t ns) 177 end 178 | _ => raise SMTLIB_PARSE ("bad Z3 proof format", p)) 179 180fun dest_name (SMTLIB.Sym name) = name 181 | dest_name t = raise SMTLIB_PARSE ("bad name", t) 182 183fun dest_seq (SMTLIB.S ts) = ts 184 | dest_seq t = raise SMTLIB_PARSE ("bad Z3 proof format", t) 185 186fun parse' (SMTLIB.S (SMTLIB.Sym "set-logic" :: _) :: ts) cx = parse' ts cx 187 | parse' (SMTLIB.S [SMTLIB.Sym "declare-fun", n, tys, ty] :: ts) cx = 188 let 189 val name = dest_name n 190 val Ts = map (type_of cx) (dest_seq tys) 191 val T = type_of cx ty 192 in parse' ts (declare_fun name (Ts ---> T) cx) end 193 | parse' (SMTLIB.S [SMTLIB.Sym "proof", p] :: _) cx = node_of p cx 194 | parse' ts _ = raise SMTLIB_PARSE ("bad Z3 proof declarations", SMTLIB.S ts) 195 196fun parse_proof typs funs lines ctxt = 197 let 198 val ts = dest_seq (SMTLIB.parse lines) 199 val (node, cx) = parse' ts (empty_context ctxt typs funs) 200 in (node, ctxt_of cx) end 201 handle SMTLIB.PARSE (l, msg) => error ("parsing error at line " ^ string_of_int l ^ ": " ^ msg) 202 | SMTLIB_PARSE (msg, t) => error (msg ^ ": " ^ SMTLIB.str_of t) 203 204 205(* handling of bound variables *) 206 207fun subst_of tyenv = 208 let fun add (ix, (S, T)) = cons (TVar (ix, S), T) 209 in Vartab.fold add tyenv [] end 210 211fun substTs_same subst = 212 let val applyT = Same.function (AList.lookup (op =) subst) 213 in Term_Subst.map_atypsT_same applyT end 214 215fun subst_types ctxt env bounds t = 216 let 217 val match = Sign.typ_match (Proof_Context.theory_of ctxt) 218 219 fun objT_of bound = 220 (case Symtab.lookup env bound of 221 SOME objT => objT 222 | NONE => raise Fail ("Replaying the proof trace produced by Z3 failed: " ^ 223 "the bound " ^ quote bound ^ " is undeclared; this indicates a bug in Z3")) 224 225 val t' = singleton (Variable.polymorphic ctxt) t 226 val patTs = map snd (Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t') 227 val objTs = map objT_of bounds 228 val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty) 229 in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end 230 231fun eq_quant (\<^const_name>\<open>HOL.All\<close>, _) (\<^const_name>\<open>HOL.All\<close>, _) = true 232 | eq_quant (\<^const_name>\<open>HOL.Ex\<close>, _) (\<^const_name>\<open>HOL.Ex\<close>, _) = true 233 | eq_quant _ _ = false 234 235fun opp_quant (\<^const_name>\<open>HOL.All\<close>, _) (\<^const_name>\<open>HOL.Ex\<close>, _) = true 236 | opp_quant (\<^const_name>\<open>HOL.Ex\<close>, _) (\<^const_name>\<open>HOL.All\<close>, _) = true 237 | opp_quant _ _ = false 238 239fun with_quant pred i (Const q1 $ Abs (_, T1, t1), Const q2 $ Abs (_, T2, t2)) = 240 if pred q1 q2 andalso T1 = T2 then 241 let val t = Var (("", i), T1) 242 in SOME (apply2 Term.subst_bound ((t, t1), (t, t2))) end 243 else NONE 244 | with_quant _ _ _ = NONE 245 246fun dest_quant_pair i (\<^term>\<open>HOL.Not\<close> $ t1, t2) = 247 Option.map (apfst HOLogic.mk_not) (with_quant opp_quant i (t1, t2)) 248 | dest_quant_pair i (t1, t2) = with_quant eq_quant i (t1, t2) 249 250fun dest_quant i t = 251 (case dest_quant_pair i (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) of 252 SOME (t1, t2) => HOLogic.mk_Trueprop (HOLogic.mk_eq (t1, t2)) 253 | NONE => raise TERM ("lift_quant", [t])) 254 255fun match_types ctxt pat obj = 256 (Vartab.empty, Vartab.empty) 257 |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, obj) 258 259fun strip_match ctxt pat i obj = 260 (case try (match_types ctxt pat) obj of 261 SOME (tyenv, _) => subst_of tyenv 262 | NONE => strip_match ctxt pat (i + 1) (dest_quant i obj)) 263 264fun dest_all i (Const (\<^const_name>\<open>Pure.all\<close>, _) $ (a as Abs (_, T, _))) = 265 dest_all (i + 1) (Term.betapply (a, Var (("", i), T))) 266 | dest_all i t = (i, t) 267 268fun dest_alls t = dest_all (Term.maxidx_of_term t + 1) t 269 270fun match_rule ctxt env (Z3_Node {bounds = bs', concl = t', ...}) bs t = 271 let 272 val t'' = singleton (Variable.polymorphic ctxt) t' 273 val (i, obj) = dest_alls (subst_types ctxt env bs t) 274 in 275 (case try (strip_match ctxt (snd (dest_alls t'')) i) obj of 276 NONE => NONE 277 | SOME subst => 278 let 279 val applyT = Same.commit (substTs_same subst) 280 val patTs = map snd (Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t'') 281 in SOME (Symtab.make (bs' ~~ map applyT patTs)) end) 282 end 283 284 285(* linearizing proofs and resolving types of bound variables *) 286 287fun has_step (tab, _) = Inttab.defined tab 288 289fun add_step id rule bounds concl is_fix_step ids (tab, sts) = 290 let val step = mk_step id rule ids concl bounds is_fix_step 291 in (id, (Inttab.update (id, ()) tab, step :: sts)) end 292 293fun is_fix_rule rule prems = 294 member (op =) [Quant_Intro, Nnf_Pos, Nnf_Neg] rule andalso length prems = 1 295 296fun lin_proof ctxt env (Z3_Node {id, rule, prems, concl, bounds}) steps = 297 if has_step steps id then (id, steps) 298 else 299 let 300 val t = subst_types ctxt env bounds concl 301 val add = add_step id rule bounds t 302 fun rec_apply e b = fold_map (lin_proof ctxt e) prems #-> add b 303 in 304 if is_fix_rule rule prems then 305 (case match_rule ctxt env (hd prems) bounds t of 306 NONE => rec_apply env false steps 307 | SOME env' => rec_apply env' true steps) 308 else rec_apply env false steps 309 end 310 311fun linearize ctxt node = 312 rev (snd (snd (lin_proof ctxt Symtab.empty node (Inttab.empty, [])))) 313 314 315(* overall proof parser *) 316 317fun parse typs funs lines ctxt = 318 let val (node, ctxt') = parse_proof typs funs lines ctxt 319 in (linearize ctxt' node, ctxt') end 320 321end; 322