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