equal
deleted
inserted
replaced
1163 expect} t negate = |
1163 expect} t negate = |
1164 let |
1164 let |
1165 (* unit -> unit *) |
1165 (* unit -> unit *) |
1166 fun wrapper () = |
1166 fun wrapper () = |
1167 let |
1167 let |
|
1168 val timer = Timer.startRealTimer () |
1168 val u = unfold_defs thy t |
1169 val u = unfold_defs thy t |
1169 val _ = Output.tracing ("Unfolded term: " ^ |
1170 val _ = Output.tracing ("Unfolded term: " ^ |
1170 Syntax.string_of_term_global thy u) |
1171 Syntax.string_of_term_global thy u) |
1171 val axioms = collect_axioms thy u |
1172 val axioms = collect_axioms thy u |
1172 (* Term.typ list *) |
1173 (* Term.typ list *) |
1199 else |
1200 else |
1200 () |
1201 () |
1201 (* (Term.typ * int) list -> string *) |
1202 (* (Term.typ * int) list -> string *) |
1202 fun find_model_loop universe = |
1203 fun find_model_loop universe = |
1203 let |
1204 let |
|
1205 val msecs_spent = Time.toMilliseconds (Timer.checkRealTimer timer) |
|
1206 val _ = maxtime = 0 orelse msecs_spent < 1000 * maxtime |
|
1207 orelse raise TimeLimit.TimeOut |
1204 val init_model = (universe, []) |
1208 val init_model = (universe, []) |
1205 val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, |
1209 val init_args = {maxvars = maxvars, def_eq = false, next_idx = 1, |
1206 bounds = [], wellformed = True} |
1210 bounds = [], wellformed = True} |
1207 val _ = Output.tracing ("Translating term (sizes: " |
1211 val _ = Output.tracing ("Translating term (sizes: " |
1208 ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") |
1212 ^ commas (map (fn (_, n) => string_of_int n) universe) ^ ") ...") |