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