1(*  Title:      HOL/Tools/SMT/smt_replay.ML
2    Author:     Sascha Boehme, TU Muenchen
3    Author:     Jasmin Blanchette, TU Muenchen
4    Author:     Mathias Fleury, MPII
5
6Shared library for parsing and replay.
7*)
8
9signature SMT_REPLAY =
10sig
11  (*theorem nets*)
12  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
13  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
14
15  (*proof combinators*)
16  val under_assumption: (thm -> thm) -> cterm -> thm
17  val discharge: thm -> thm -> thm
18
19  (*a faster COMP*)
20  type compose_data = cterm list * (cterm -> cterm list) * thm
21  val precompose: (cterm -> cterm list) -> thm -> compose_data
22  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
23  val compose: compose_data -> thm -> thm
24
25  (*simpset*)
26  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
27  val make_simpset: Proof.context -> thm list -> simpset
28
29  (*assertion*)
30  val add_asserted:  ('a * ('b * thm) -> 'c -> 'c) ->
31    'c -> ('d -> 'a * 'e * term * 'b) -> ('e -> bool) -> Proof.context -> thm list ->
32    (int * thm) list -> 'd list -> Proof.context ->
33    ((int * ('a * thm)) list * thm list) * (Proof.context * 'c)
34  
35  (*statistics*)
36  val pretty_statistics: string -> int -> int list Symtab.table -> Pretty.T
37  val intermediate_statistics: Proof.context -> Timing.start -> int -> int -> unit
38
39  (*theorem transformation*)
40  val varify: Proof.context -> thm -> thm
41  val params_of: term -> (string * typ) list
42end;
43
44structure SMT_Replay : SMT_REPLAY =
45struct
46
47(* theorem nets *)
48
49fun thm_net_of f xthms =
50  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
51  in fold insert xthms Net.empty end
52
53fun maybe_instantiate ct thm =
54  try Thm.first_order_match (Thm.cprop_of thm, ct)
55  |> Option.map (fn inst => Thm.instantiate inst thm)
56
57local
58  fun instances_from_net match f net ct =
59    let
60      val lookup = if match then Net.match_term else Net.unify_term
61      val xthms = lookup net (Thm.term_of ct)
62      fun select ct = map_filter (f (maybe_instantiate ct)) xthms
63      fun select' ct =
64        let val thm = Thm.trivial ct
65        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
66    in (case select ct of [] => select' ct | xthms' => xthms') end
67in
68
69fun net_instances net =
70  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
71    net
72
73end
74
75
76(* proof combinators *)
77
78fun under_assumption f ct =
79  let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
80
81fun discharge p pq = Thm.implies_elim pq p
82
83
84(* a faster COMP *)
85
86type compose_data = cterm list * (cterm -> cterm list) * thm
87
88fun list2 (x, y) = [x, y]
89
90fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
91fun precompose2 f rule : compose_data = precompose (list2 o f) rule
92
93fun compose (cvs, f, rule) thm =
94  discharge thm
95    (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
96
97
98(* simpset *)
99
100local
101  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
102  val antisym_le2 = mk_meta_eq @{thm order_class.antisym_conv2}
103  val antisym_less1 = mk_meta_eq @{thm order_class.antisym_conv1}
104  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
105
106  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
107  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
108    | dest_binop t = raise TERM ("dest_binop", [t])
109
110  fun prove_antisym_le ctxt ct =
111    let
112      val (le, r, s) = dest_binop (Thm.term_of ct)
113      val less = Const (\<^const_name>\<open>less\<close>, Term.fastype_of le)
114      val prems = Simplifier.prems_of ctxt
115    in
116      (case find_first (eq_prop (le $ s $ r)) prems of
117        NONE =>
118          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
119          |> Option.map (fn thm => thm RS antisym_less1)
120      | SOME thm => SOME (thm RS antisym_le1))
121    end
122    handle THM _ => NONE
123
124  fun prove_antisym_less ctxt ct =
125    let
126      val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
127      val le = Const (\<^const_name>\<open>less_eq\<close>, Term.fastype_of less)
128      val prems = Simplifier.prems_of ctxt
129    in
130      (case find_first (eq_prop (le $ r $ s)) prems of
131        NONE =>
132          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
133          |> Option.map (fn thm => thm RS antisym_less2)
134      | SOME thm => SOME (thm RS antisym_le2))
135  end
136  handle THM _ => NONE
137
138  val basic_simpset =
139    simpset_of (put_simpset HOL_ss \<^context>
140      addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
141        arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
142      addsimprocs [\<^simproc>\<open>numeral_divmod\<close>,
143        Simplifier.make_simproc \<^context> "fast_int_arith"
144         {lhss = [\<^term>\<open>(m::int) < n\<close>, \<^term>\<open>(m::int) \<le> n\<close>, \<^term>\<open>(m::int) = n\<close>],
145          proc = K Lin_Arith.simproc},
146        Simplifier.make_simproc \<^context> "antisym_le"
147         {lhss = [\<^term>\<open>(x::'a::order) \<le> y\<close>],
148          proc = K prove_antisym_le},
149        Simplifier.make_simproc \<^context> "antisym_less"
150         {lhss = [\<^term>\<open>\<not> (x::'a::linorder) < y\<close>],
151          proc = K prove_antisym_less}])
152
153  structure Simpset = Generic_Data
154  (
155    type T = simpset
156    val empty = basic_simpset
157    val extend = I
158    val merge = Simplifier.merge_ss
159  )
160in
161
162fun add_simproc simproc context =
163  Simpset.map (simpset_map (Context.proof_of context)
164    (fn ctxt => ctxt addsimprocs [simproc])) context
165
166fun make_simpset ctxt rules =
167  simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
168
169end
170
171local
172  val remove_trigger = mk_meta_eq @{thm trigger_def}
173  val remove_fun_app = mk_meta_eq @{thm fun_app_def}
174
175  fun rewrite_conv _ [] = Conv.all_conv
176    | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
177
178  val rewrite_true_rule = @{lemma "True \<equiv> \<not> False" by simp}
179  val prep_rules = [@{thm Let_def}, remove_trigger, remove_fun_app, rewrite_true_rule]
180
181  fun rewrite _ [] = I
182    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
183
184  fun lookup_assm assms_net ct =
185    net_instances assms_net ct
186    |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
187in
188
189fun add_asserted tab_update tab_empty p_extract cond outer_ctxt rewrite_rules assms steps ctxt0 =
190  let
191    val eqs = map (rewrite ctxt0 [rewrite_true_rule]) rewrite_rules
192    val eqs' = union Thm.eq_thm eqs prep_rules
193
194    val assms_net =
195      assms
196      |> map (apsnd (rewrite ctxt0 eqs'))
197      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
198      |> thm_net_of snd
199
200    fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
201
202    fun assume thm ctxt =
203      let
204        val ct = Thm.cprem_of thm 1
205        val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
206      in (thm' RS thm, ctxt') end
207
208    fun add1 id fixes thm1 ((i, th), exact) ((iidths, thms), (ctxt, ptab)) =
209      let
210        val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt
211        val thms' = if exact then thms else th :: thms
212      in (((i, (id, th)) :: iidths, thms'), (ctxt', tab_update (id, (fixes, thm)) ptab)) end
213
214    fun add step
215        (cx as ((iidths, thms), (ctxt, ptab))) =
216      let val (id, rule, concl, fixes) = p_extract step in
217        if (*Z3_Proof.is_assumption rule andalso rule <> Z3_Proof.Hypothesis*) cond rule then
218          let
219            val ct = Thm.cterm_of ctxt concl
220            val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
221            val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
222          in
223            (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
224              [] =>
225                let val (thm, ctxt') = assume thm1 ctxt
226                in ((iidths, thms), (ctxt', tab_update (id, (fixes, thm)) ptab)) end
227            | ithms => fold (add1 id fixes thm1) ithms cx)
228          end
229        else
230          cx
231      end
232  in fold add steps (([], []), (ctxt0, tab_empty)) end
233
234end
235
236fun params_of t = Term.strip_qnt_vars \<^const_name>\<open>Pure.all\<close> t
237
238fun varify ctxt thm =
239  let
240    val maxidx = Thm.maxidx_of thm + 1
241    val vs = params_of (Thm.prop_of thm)
242    val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
243  in Drule.forall_elim_list (map (Thm.cterm_of ctxt) vars) thm end
244
245fun intermediate_statistics ctxt start total =
246  SMT_Config.statistics_msg ctxt (fn current =>
247    "Reconstructed " ^ string_of_int current ^ " of " ^ string_of_int total ^ " steps in " ^
248    string_of_int (Time.toMilliseconds (#elapsed (Timing.result start))) ^ " ms")
249
250fun pretty_statistics solver total stats =
251  let
252    fun mean_of is =
253      let
254        val len = length is
255        val mid = len div 2
256      in if len mod 2 = 0 then (nth is (mid - 1) + nth is mid) div 2 else nth is mid end
257    fun pretty_item name p = Pretty.item (Pretty.separate ":" [Pretty.str name, p])
258    fun pretty (name, milliseconds) = pretty_item name (Pretty.block (Pretty.separate "," [
259      Pretty.str (string_of_int (length milliseconds) ^ " occurrences") ,
260      Pretty.str (string_of_int (mean_of milliseconds) ^ " ms mean time"),
261      Pretty.str (string_of_int (fold Integer.max milliseconds 0) ^ " ms maximum time"),
262      Pretty.str (string_of_int (fold Integer.add milliseconds 0) ^ " ms total time")]))
263  in
264    Pretty.big_list (solver ^ " proof reconstruction statistics:") (
265      pretty_item "total time" (Pretty.str (string_of_int total ^ " ms")) ::
266      map pretty (Symtab.dest stats))
267  end
268
269end;
270