author  blanchet 
Tue, 27 Oct 2009 19:00:17 +0100  
changeset 33558  a2db56854b83 
parent 33556  cba22e2999d5 
child 33561  ab01b72715ef 
permissions  rwrr 
33192  1 
(* Title: HOL/Nitpick/Tools/nitpick.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Copyright 2008, 2009 

4 

5 
Finite model generation for HOL formulas using Kodkod. 

6 
*) 

7 

8 
signature NITPICK = 

9 
sig 

10 
type params = { 

11 
cards_assigns: (typ option * int list) list, 

12 
maxes_assigns: (styp option * int list) list, 

13 
iters_assigns: (styp option * int list) list, 

14 
bisim_depths: int list, 

15 
boxes: (typ option * bool option) list, 

16 
monos: (typ option * bool option) list, 

17 
wfs: (styp option * bool option) list, 

18 
sat_solver: string, 

19 
blocking: bool, 

20 
falsify: bool, 

21 
debug: bool, 

22 
verbose: bool, 

23 
overlord: bool, 

24 
user_axioms: bool option, 

25 
assms: bool, 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

26 
merge_type_vars: bool, 
33192  27 
destroy_constrs: bool, 
28 
specialize: bool, 

29 
skolemize: bool, 

30 
star_linear_preds: bool, 

31 
uncurry: bool, 

32 
fast_descrs: bool, 

33 
peephole_optim: bool, 

34 
timeout: Time.time option, 

35 
tac_timeout: Time.time option, 

36 
sym_break: int, 

37 
sharing_depth: int, 

38 
flatten_props: bool, 

39 
max_threads: int, 

40 
show_skolems: bool, 

41 
show_datatypes: bool, 

42 
show_consts: bool, 

43 
evals: term list, 

44 
formats: (term option * int list) list, 

45 
max_potential: int, 

46 
max_genuine: int, 

47 
check_potential: bool, 

48 
check_genuine: bool, 

49 
batch_size: int, 

50 
expect: string} 

51 

52 
val register_frac_type : string > (string * string) list > theory > theory 

53 
val unregister_frac_type : string > theory > theory 

54 
val register_codatatype : typ > string > styp list > theory > theory 

55 
val unregister_codatatype : typ > theory > theory 

56 
val pick_nits_in_term : 

57 
Proof.state > params > bool > term list > term > string * Proof.state 

58 
val pick_nits_in_subgoal : 

59 
Proof.state > params > bool > int > string * Proof.state 

60 
end; 

61 

62 
structure Nitpick : NITPICK = 

63 
struct 

64 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

65 
open Nitpick_Util 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

66 
open Nitpick_HOL 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

67 
open Nitpick_Mono 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

68 
open Nitpick_Scope 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

69 
open Nitpick_Peephole 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

70 
open Nitpick_Rep 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

71 
open Nitpick_Nut 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

72 
open Nitpick_Kodkod 
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

73 
open Nitpick_Model 
33192  74 

75 
type params = { 

76 
cards_assigns: (typ option * int list) list, 

77 
maxes_assigns: (styp option * int list) list, 

78 
iters_assigns: (styp option * int list) list, 

79 
bisim_depths: int list, 

80 
boxes: (typ option * bool option) list, 

81 
monos: (typ option * bool option) list, 

82 
wfs: (styp option * bool option) list, 

83 
sat_solver: string, 

84 
blocking: bool, 

85 
falsify: bool, 

86 
debug: bool, 

87 
verbose: bool, 

88 
overlord: bool, 

89 
user_axioms: bool option, 

90 
assms: bool, 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

91 
merge_type_vars: bool, 
33192  92 
destroy_constrs: bool, 
93 
specialize: bool, 

94 
skolemize: bool, 

95 
star_linear_preds: bool, 

96 
uncurry: bool, 

97 
fast_descrs: bool, 

98 
peephole_optim: bool, 

99 
timeout: Time.time option, 

100 
tac_timeout: Time.time option, 

101 
sym_break: int, 

102 
sharing_depth: int, 

103 
flatten_props: bool, 

104 
max_threads: int, 

105 
show_skolems: bool, 

106 
show_datatypes: bool, 

107 
show_consts: bool, 

108 
evals: term list, 

109 
formats: (term option * int list) list, 

110 
max_potential: int, 

111 
max_genuine: int, 

112 
check_potential: bool, 

113 
check_genuine: bool, 

114 
batch_size: int, 

115 
expect: string} 

116 

117 
type problem_extension = { 

118 
free_names: nut list, 

119 
sel_names: nut list, 

120 
nonsel_names: nut list, 

121 
rel_table: nut NameTable.table, 

122 
liberal: bool, 

123 
scope: scope, 

124 
core: Kodkod.formula, 

125 
defs: Kodkod.formula list} 

126 

127 
type rich_problem = Kodkod.problem * problem_extension 

128 

129 
(* Proof.context > string > term list > Pretty.T list *) 

130 
fun pretties_for_formulas _ _ [] = [] 

131 
 pretties_for_formulas ctxt s ts = 

132 
[Pretty.str (s ^ plural_s_for_list ts ^ ":"), 

133 
Pretty.indent indent_size (Pretty.chunks 

134 
(map2 (fn j => fn t => 

135 
Pretty.block [t > shorten_const_names_in_term 

136 
> Syntax.pretty_term ctxt, 

137 
Pretty.str (if j = 1 then "." else ";")]) 

138 
(length ts downto 1) ts))] 

139 

140 
val max_liberal_delay_ms = 200 

141 
val max_liberal_delay_percent = 2 

142 

143 
(* Time.time option > int *) 

144 
fun liberal_delay_for_timeout NONE = max_liberal_delay_ms 

145 
 liberal_delay_for_timeout (SOME timeout) = 

146 
Int.max (0, Int.min (max_liberal_delay_ms, 

147 
Time.toMilliseconds timeout 

148 
* max_liberal_delay_percent div 100)) 

149 

150 
(* Time.time option > bool *) 

151 
fun passed_deadline NONE = false 

152 
 passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS 

153 

154 
(* ('a * bool option) list > bool *) 

155 
fun none_true asgns = forall (not_equal (SOME true) o snd) asgns 

156 

157 
val weaselly_sorts = 

158 
[@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus}, 

159 
@{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn}, 

160 
@{sort ord}, @{sort eq}, @{sort number}] 

161 
(* theory > typ > bool *) 

162 
fun is_tfree_with_weaselly_sort thy (TFree (_, S)) = 

163 
exists (curry (Sign.subsort thy) S) weaselly_sorts 

164 
 is_tfree_with_weaselly_sort _ _ = false 

165 
(* theory term > bool *) 

166 
val has_weaselly_sorts = 

167 
exists_type o exists_subtype o is_tfree_with_weaselly_sort 

168 

169 
(* Time.time > Proof.state > params > bool > term > string * Proof.state *) 

170 
fun pick_them_nits_in_term deadline state (params : params) auto orig_assm_ts 

171 
orig_t = 

172 
let 

173 
val timer = Timer.startRealTimer () 

174 
val thy = Proof.theory_of state 

175 
val ctxt = Proof.context_of state 

176 
val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes, 

177 
monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord, 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

178 
user_axioms, assms, merge_type_vars, destroy_constrs, specialize, 
33192  179 
skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim, 
180 
tac_timeout, sym_break, sharing_depth, flatten_props, max_threads, 

181 
show_skolems, show_datatypes, show_consts, evals, formats, 

182 
max_potential, max_genuine, check_potential, check_genuine, batch_size, 

183 
...} = 

184 
params 

185 
val state_ref = Unsynchronized.ref state 

186 
(* Pretty.T > unit *) 

187 
val pprint = 

188 
if auto then 

189 
Unsynchronized.change state_ref o Proof.goal_message o K 

190 
o curry Pretty.blk 0 o cons (Pretty.str "") o single 

191 
o Pretty.mark Markup.hilite 

192 
else 

193 
priority o Pretty.string_of 

194 
(* (unit > Pretty.T) > unit *) 

195 
fun pprint_m f = () > not auto ? pprint o f 

196 
fun pprint_v f = () > verbose ? pprint o f 

197 
fun pprint_d f = () > debug ? pprint o f 

198 
(* string > unit *) 

199 
val print = pprint o curry Pretty.blk 0 o pstrs 

200 
(* (unit > string) > unit *) 

201 
fun print_m f = pprint_m (curry Pretty.blk 0 o pstrs o f) 

202 
fun print_v f = pprint_v (curry Pretty.blk 0 o pstrs o f) 

203 
fun print_d f = pprint_d (curry Pretty.blk 0 o pstrs o f) 

204 

205 
(* unit > unit *) 

206 
fun check_deadline () = 

207 
if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut 

208 
else () 

209 
(* unit > 'a *) 

210 
fun do_interrupted () = 

211 
if passed_deadline deadline then raise TimeLimit.TimeOut 

212 
else raise Interrupt 

213 

214 
val _ = print_m (K "Nitpicking...") 

215 
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False}) 

216 
else orig_t 

217 
val assms_t = if assms orelse auto then 

218 
Logic.mk_conjunction_list (neg_t :: orig_assm_ts) 

219 
else 

220 
neg_t 

221 
val (assms_t, evals) = 

222 
assms_t :: evals 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

223 
> merge_type_vars ? merge_type_vars_in_terms 
33192  224 
> hd pairf tl 
225 
val original_max_potential = max_potential 

226 
val original_max_genuine = max_genuine 

227 
(* 

228 
val _ = priority ("*** " ^ Syntax.string_of_term ctxt orig_t) 

229 
val _ = List.app (fn t => priority ("*** " ^ Syntax.string_of_term ctxt t)) 

230 
orig_assm_ts 

231 
*) 

232 
val max_bisim_depth = fold Integer.max bisim_depths ~1 

233 
val case_names = case_const_names thy 

234 
val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy 

235 
val def_table = const_def_table ctxt defs 

236 
val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs) 

237 
val simp_table = Unsynchronized.ref (const_simp_table ctxt) 

238 
val psimp_table = const_psimp_table ctxt 

239 
val intro_table = inductive_intro_table ctxt def_table 

240 
val ground_thm_table = ground_theorem_table thy 

241 
val ersatz_table = ersatz_table thy 

242 
val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) = 

243 
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes, 

244 
user_axioms = user_axioms, debug = debug, wfs = wfs, 

245 
destroy_constrs = destroy_constrs, specialize = specialize, 

246 
skolemize = skolemize, star_linear_preds = star_linear_preds, 

247 
uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout, 

248 
evals = evals, case_names = case_names, def_table = def_table, 

249 
nondef_table = nondef_table, user_nondefs = user_nondefs, 

250 
simp_table = simp_table, psimp_table = psimp_table, 

251 
intro_table = intro_table, ground_thm_table = ground_thm_table, 

252 
ersatz_table = ersatz_table, skolems = Unsynchronized.ref [], 

253 
special_funs = Unsynchronized.ref [], 

254 
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []} 

255 
val frees = Term.add_frees assms_t [] 

256 
val _ = null (Term.add_tvars assms_t []) 

257 
orelse raise NOT_SUPPORTED "schematic type variables" 

258 
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)), 

259 
core_t) = preprocess_term ext_ctxt assms_t 

260 
val got_all_user_axioms = 

261 
got_all_mono_user_axioms andalso no_poly_user_axioms 

262 

263 
(* styp * (bool * bool) > unit *) 

264 
fun print_wf (x, (gfp, wf)) = 

265 
pprint (Pretty.blk (0, 

266 
pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"") 

267 
@ Syntax.pretty_term ctxt (Const x) :: 

268 
pstrs (if wf then 

269 
"\" was proved wellfounded. Nitpick can compute it \ 

270 
\efficiently." 

271 
else 

272 
"\" could not be proved wellfounded. Nitpick might need to \ 

273 
\unroll it."))) 

274 
val _ = if verbose then List.app print_wf (!wf_cache) else () 

275 
val _ = 

276 
pprint_d (fn () => 

277 
Pretty.chunks 

278 
(pretties_for_formulas ctxt "Preprocessed formula" [core_t] @ 

279 
pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @ 

280 
pretties_for_formulas ctxt "Relevant nondefinitional axiom" 

281 
nondef_ts)) 

282 
val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts) 

283 
handle TYPE (_, Ts, ts) => 

284 
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) 

285 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

286 
val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

287 
val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

288 
def_ts 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

289 
val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

290 
nondef_ts 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

291 
val (free_names, const_names) = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

292 
fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], []) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

293 
val (sel_names, nonsel_names) = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

294 
List.partition (is_sel o nickname_of) const_names 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

295 
val would_be_genuine = got_all_user_axioms andalso none_true wfs 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

296 
(* 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

297 
val _ = List.app (priority o string_for_nut ctxt) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

298 
(core_u :: def_us @ nondef_us) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

299 
*) 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

300 

33192  301 
val unique_scope = forall (equal 1 o length o snd) cards_assigns 
302 
(* typ > bool *) 

303 
fun is_free_type_monotonic T = 

304 
unique_scope orelse 

305 
case triple_lookup (type_match thy) monos T of 

306 
SOME (SOME b) => b 

307 
 _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t 

308 
fun is_datatype_monotonic T = 

309 
unique_scope orelse 

310 
case triple_lookup (type_match thy) monos T of 

311 
SOME (SOME b) => b 

312 
 _ => 

313 
not (is_pure_typedef thy T) orelse is_univ_typedef thy T 

314 
orelse is_number_type thy T 

315 
orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

316 
fun is_datatype_shallow T = 
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

317 
not (exists (equal T o domain_type o type_of) sel_names) 
33192  318 
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) 
319 
> sort TermOrd.typ_ord 

320 
val (all_dataTs, all_free_Ts) = 

321 
List.partition (is_integer_type orf is_datatype thy) Ts 

322 
val (mono_dataTs, nonmono_dataTs) = 

323 
List.partition is_datatype_monotonic all_dataTs 

324 
val (mono_free_Ts, nonmono_free_Ts) = 

325 
List.partition is_free_type_monotonic all_free_Ts 

326 

327 
val _ = 

328 
if not unique_scope andalso not (null mono_free_Ts) then 

329 
print_v (fn () => 

330 
let 

331 
val ss = map (quote o string_for_type ctxt) mono_free_Ts 

332 
in 

333 
"The type" ^ plural_s_for_list ss ^ " " ^ 

334 
space_implode " " (serial_commas "and" ss) ^ " " ^ 

335 
(if none_true monos then 

336 
"passed the monotonicity test" 

337 
else 

338 
(if length ss = 1 then "is" else "are") ^ 

339 
" considered monotonic") ^ 

340 
". Nitpick might be able to skip some scopes." 

341 
end) 

342 
else 

343 
() 

344 
val mono_Ts = mono_dataTs @ mono_free_Ts 

345 
val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

346 
val shallow_dataTs = filter is_datatype_shallow mono_dataTs 
33192  347 
(* 
348 
val _ = priority "Monotonic datatypes:" 

349 
val _ = List.app (priority o string_for_type ctxt) mono_dataTs 

350 
val _ = priority "Nonmonotonic datatypes:" 

351 
val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs 

352 
val _ = priority "Monotonic free types:" 

353 
val _ = List.app (priority o string_for_type ctxt) mono_free_Ts 

354 
val _ = priority "Nonmonotonic free types:" 

355 
val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts 

356 
*) 

357 

358 
val need_incremental = Int.max (max_potential, max_genuine) >= 2 

359 
val effective_sat_solver = 

360 
if sat_solver <> "smart" then 

361 
if need_incremental andalso 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

362 
not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then 
33192  363 
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ 
364 
\be used instead of " ^ quote sat_solver ^ ".")); 

365 
"SAT4J") 

366 
else 

367 
sat_solver 

368 
else 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

369 
Kodkod_SAT.smart_sat_solver_name need_incremental 
33192  370 
val _ = 
371 
if sat_solver = "smart" then 

372 
print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^ 

373 
". The following" ^ 

374 
(if need_incremental then " incremental " else " ") ^ 

375 
"solvers are configured: " ^ 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

376 
commas (map quote (Kodkod_SAT.configured_sat_solvers 
33192  377 
need_incremental)) ^ ".") 
378 
else 

379 
() 

380 

381 
val too_big_scopes = Unsynchronized.ref [] 

382 

383 
(* bool > scope > rich_problem option *) 

384 
fun problem_for_scope liberal 

385 
(scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) = 

386 
let 

387 
val _ = not (exists (fn other => scope_less_eq other scope) 

388 
(!too_big_scopes)) 

389 
orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\ 

390 
\problem_for_scope", "too big scope") 

391 
(* 

392 
val _ = priority "Offsets:" 

393 
val _ = List.app (fn (T, j0) => 

394 
priority (string_for_type ctxt T ^ " = " ^ 

395 
string_of_int j0)) 

396 
(Typtab.dest ofs) 

397 
*) 

398 
val all_precise = forall (is_precise_type datatypes) Ts 

399 
(* nut list > rep NameTable.table > nut list * rep NameTable.table *) 

400 
val repify_consts = choose_reps_for_consts scope all_precise 

401 
val main_j0 = offset_of_type ofs bool_T 

402 
val (nat_card, nat_j0) = spec_of_type scope nat_T 

403 
val (int_card, int_j0) = spec_of_type scope int_T 

404 
val _ = forall (equal main_j0) [nat_j0, int_j0] 

405 
orelse raise BAD ("Nitpick.pick_them_nits_in_term.\ 

406 
\problem_for_scope", "bad offsets") 

407 
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0 

408 
val (free_names, rep_table) = 

409 
choose_reps_for_free_vars scope free_names NameTable.empty 

410 
val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table 

411 
val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table 

412 
val min_highest_arity = 

413 
NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1 

414 
val min_univ_card = 

415 
NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table 

416 
(univ_card nat_card int_card main_j0 [] Kodkod.True) 

417 
val _ = check_arity min_univ_card min_highest_arity 

418 

419 
val core_u = choose_reps_in_nut scope liberal rep_table false core_u 

420 
val def_us = map (choose_reps_in_nut scope liberal rep_table true) 

421 
def_us 

422 
val nondef_us = map (choose_reps_in_nut scope liberal rep_table false) 

423 
nondef_us 

424 
(* 

425 
val _ = List.app (priority o string_for_nut ctxt) 

426 
(free_names @ sel_names @ nonsel_names @ 

427 
core_u :: def_us @ nondef_us) 

428 
*) 

429 
val (free_rels, pool, rel_table) = 

430 
rename_free_vars free_names initial_pool NameTable.empty 

431 
val (sel_rels, pool, rel_table) = 

432 
rename_free_vars sel_names pool rel_table 

433 
val (other_rels, pool, rel_table) = 

434 
rename_free_vars nonsel_names pool rel_table 

435 
val core_u = rename_vars_in_nut pool rel_table core_u 

436 
val def_us = map (rename_vars_in_nut pool rel_table) def_us 

437 
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us 

438 
(* nut > Kodkod.formula *) 

439 
val to_f = kodkod_formula_from_nut ofs liberal kk 

440 
val core_f = to_f core_u 

441 
val def_fs = map to_f def_us 

442 
val nondef_fs = map to_f nondef_us 

443 
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f 

444 
val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^ 

445 
PrintMode.setmp [] multiline_string_for_scope scope 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

446 
val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver 
33192  447 
> snd 
448 
val delay = if liberal then 

449 
Option.map (fn time => Time. (time, Time.now ())) 

450 
deadline 

451 
> liberal_delay_for_timeout 

452 
else 

453 
0 

454 
val settings = [("solver", commas (map quote kodkod_sat_solver)), 

455 
("skolem_depth", "1"), 

456 
("bit_width", "16"), 

457 
("symmetry_breaking", signed_string_of_int sym_break), 

458 
("sharing", signed_string_of_int sharing_depth), 

459 
("flatten", Bool.toString flatten_props), 

460 
("delay", signed_string_of_int delay)] 

461 
val plain_rels = free_rels @ other_rels 

462 
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels 

463 
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels 

464 
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels 

465 
val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk 

466 
rel_table datatypes 

467 
val declarative_axioms = plain_axioms @ dtype_axioms 

468 
val univ_card = univ_card nat_card int_card main_j0 

469 
(plain_bounds @ sel_bounds) formula 

470 
val built_in_bounds = bounds_for_built_in_rels_in_formula debug 

471 
univ_card nat_card int_card main_j0 formula 

472 
val bounds = built_in_bounds @ plain_bounds @ sel_bounds 

473 
> not debug ? merge_bounds 

474 
val highest_arity = 

475 
fold Integer.max (map (fst o fst) (maps fst bounds)) 0 

476 
val formula = fold_rev s_and declarative_axioms formula 

477 
val _ = if formula = Kodkod.False then () 

478 
else check_arity univ_card highest_arity 

479 
in 

480 
SOME ({comment = comment, settings = settings, univ_card = univ_card, 

481 
tuple_assigns = [], bounds = bounds, 

482 
int_bounds = sequential_int_bounds univ_card, 

483 
expr_assigns = [], formula = formula}, 

484 
{free_names = free_names, sel_names = sel_names, 

485 
nonsel_names = nonsel_names, rel_table = rel_table, 

486 
liberal = liberal, scope = scope, core = core_f, 

487 
defs = nondef_fs @ def_fs @ declarative_axioms}) 

488 
end 

489 
handle LIMIT (loc, msg) => 

33232
f93390060bbe
internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
blanchet
parents:
33192
diff
changeset

490 
if loc = "Nitpick_Kodkod.check_arity" 
33192  491 
andalso not (Typtab.is_empty ofs) then 
492 
problem_for_scope liberal 

493 
{ext_ctxt = ext_ctxt, card_assigns = card_assigns, 

494 
bisim_depth = bisim_depth, datatypes = datatypes, 

495 
ofs = Typtab.empty} 

496 
else if loc = "Nitpick.pick_them_nits_in_term.\ 

497 
\problem_for_scope" then 

498 
NONE 

499 
else 

500 
(Unsynchronized.change too_big_scopes (cons scope); 

501 
print_v (fn () => ("Limit reached: " ^ msg ^ 

502 
". Dropping " ^ (if liberal then "potential" 

503 
else "genuine") ^ 

504 
" component of scope.")); 

505 
NONE) 

506 

507 
(* int > (''a * int list list) list > ''a > Kodkod.tuple_set *) 

508 
fun tuple_set_for_rel univ_card = 

509 
Kodkod.TupleSet o map (kk_tuple debug univ_card) o the 

510 
oo AList.lookup (op =) 

511 

512 
val word_model = if falsify then "counterexample" else "model" 

513 

514 
val scopes = Unsynchronized.ref [] 

515 
val generated_scopes = Unsynchronized.ref [] 

516 
val generated_problems = Unsynchronized.ref [] 

517 
val checked_problems = Unsynchronized.ref (SOME []) 

518 
val met_potential = Unsynchronized.ref 0 

519 

520 
(* rich_problem list > int list > unit *) 

521 
fun update_checked_problems problems = 

522 
List.app (Unsynchronized.change checked_problems o Option.map o cons 

523 
o nth problems) 

524 

525 
(* bool > Kodkod.raw_bound list > problem_extension > bool option *) 

526 
fun print_and_check_model genuine bounds 

527 
({free_names, sel_names, nonsel_names, rel_table, scope, ...} 

528 
: problem_extension) = 

529 
let 

530 
val (reconstructed_model, codatatypes_ok) = 

531 
reconstruct_hol_model {show_skolems = show_skolems, 

532 
show_datatypes = show_datatypes, 

533 
show_consts = show_consts} 

534 
scope formats frees free_names sel_names nonsel_names rel_table 

535 
bounds 

536 
val would_be_genuine = would_be_genuine andalso codatatypes_ok 

537 
in 

538 
pprint (Pretty.chunks 

539 
[Pretty.blk (0, 

540 
(pstrs ("Nitpick found a" ^ 

541 
(if not genuine then " potential " 

542 
else if would_be_genuine then " " 

543 
else " likely genuine ") ^ word_model) @ 

544 
(case pretties_for_scope scope verbose of 

545 
[] => [] 

546 
 pretties => pstrs " for " @ pretties) @ 

547 
[Pretty.str ":\n"])), 

548 
Pretty.indent indent_size reconstructed_model]); 

549 
if genuine then 

550 
(if check_genuine then 

551 
(case prove_hol_model scope tac_timeout free_names sel_names 

552 
rel_table bounds assms_t of 

553 
SOME true => print ("Confirmation by \"auto\": The above " ^ 

554 
word_model ^ " is really genuine.") 

555 
 SOME false => 

556 
if would_be_genuine then 

557 
error ("A supposedly genuine " ^ word_model ^ " was shown to\ 

558 
\be spurious by \"auto\".\nThis should never happen.\n\ 

559 
\Please send a bug report to blanchet\ 

560 
\te@in.tum.de.") 

561 
else 

562 
print ("Refutation by \"auto\": The above " ^ word_model ^ 

563 
" is spurious.") 

564 
 NONE => print "No confirmation by \"auto\".") 

565 
else 

566 
(); 

567 
if has_weaselly_sorts thy orig_t then 

568 
print "Hint: Maybe you forgot a type constraint?" 

569 
else 

570 
(); 

571 
if not would_be_genuine then 

572 
if no_poly_user_axioms then 

573 
let 

574 
val options = 

575 
[] > not got_all_mono_user_axioms 

576 
? cons ("user_axioms", "\"true\"") 

577 
> not (none_true wfs) 

578 
? cons ("wf", "\"smart\" or \"false\"") 

579 
> not codatatypes_ok 

580 
? cons ("bisim_depth", "a nonnegative value") 

581 
val ss = 

582 
map (fn (name, value) => quote name ^ " set to " ^ value) 

583 
options 

584 
in 

585 
print ("Try again with " ^ 

586 
space_implode " " (serial_commas "and" ss) ^ 

587 
" to confirm that the " ^ word_model ^ " is genuine.") 

588 
end 

589 
else 

590 
print ("Nitpick is unable to guarantee the authenticity of \ 

591 
\the " ^ word_model ^ " in the presence of polymorphic \ 

592 
\axioms.") 

593 
else 

594 
(); 

595 
NONE) 

596 
else 

597 
if not genuine then 

598 
(Unsynchronized.inc met_potential; 

599 
if check_potential then 

600 
let 

601 
val status = prove_hol_model scope tac_timeout free_names 

602 
sel_names rel_table bounds assms_t 

603 
in 

604 
(case status of 

605 
SOME true => print ("Confirmation by \"auto\": The above " ^ 

606 
word_model ^ " is genuine.") 

607 
 SOME false => print ("Refutation by \"auto\": The above " ^ 

608 
word_model ^ " is spurious.") 

609 
 NONE => print "No confirmation by \"auto\"."); 

610 
status 

611 
end 

612 
else 

613 
NONE) 

614 
else 

615 
NONE 

616 
end 

617 
(* int > int > int > bool > rich_problem list > int * int * int *) 

618 
fun solve_any_problem max_potential max_genuine donno first_time problems = 

619 
let 

620 
val max_potential = Int.max (0, max_potential) 

621 
val max_genuine = Int.max (0, max_genuine) 

622 
(* bool > int * Kodkod.raw_bound list > bool option *) 

623 
fun print_and_check genuine (j, bounds) = 

624 
print_and_check_model genuine bounds (snd (nth problems j)) 

625 
val max_solutions = max_potential + max_genuine 

626 
> not need_incremental ? curry Int.min 1 

627 
in 

628 
if max_solutions <= 0 then 

629 
(0, 0, donno) 

630 
else 

631 
case Kodkod.solve_any_problem overlord deadline max_threads 

632 
max_solutions (map fst problems) of 

33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

633 
Kodkod.NotInstalled => 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

634 
(print_m (fn () => 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

635 
"Nitpick requires the external Java program Kodkodi. \ 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

636 
\To install it, download the package from Isabelle's \ 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

637 
\web page and add the \"kodkodix.y.z\" directory's \ 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

638 
\full path to \"" ^ 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

639 
Path.implode (Path.expand (Path.appends 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

640 
(Path.variable "ISABELLE_HOME" :: 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

641 
(map Path.basic ["etc", "components"])))) ^ 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

642 
"\"."); 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

643 
(max_potential, max_genuine, donno + 1)) 
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

644 
 Kodkod.Normal ([], unsat_js) => 
33192  645 
(update_checked_problems problems unsat_js; 
646 
(max_potential, max_genuine, donno)) 

647 
 Kodkod.Normal (sat_ps, unsat_js) => 

648 
let 

649 
val (lib_ps, con_ps) = 

650 
List.partition (#liberal o snd o nth problems o fst) sat_ps 

651 
in 

652 
update_checked_problems problems (unsat_js @ map fst lib_ps); 

653 
if null con_ps then 

654 
let 

655 
val num_genuine = Library.take (max_potential, lib_ps) 

656 
> map (print_and_check false) 

657 
> filter (equal (SOME true)) > length 

658 
val max_genuine = max_genuine  num_genuine 

659 
val max_potential = max_potential 

660 
 (length lib_ps  num_genuine) 

661 
in 

662 
if max_genuine <= 0 then 

663 
(0, 0, donno) 

664 
else 

665 
let 

666 
(* "co_js" is the list of conservative problems whose 

667 
liberal pendants couldn't be satisfied and hence that 

668 
most probably can't be satisfied themselves. *) 

669 
val co_js = 

670 
map (fn j => j  1) unsat_js 

671 
> filter (fn j => 

672 
j >= 0 andalso 

673 
scopes_equivalent 

674 
(#scope (snd (nth problems j))) 

675 
(#scope (snd (nth problems (j + 1))))) 

676 
val bye_js = sort_distinct int_ord (map fst sat_ps @ 

677 
unsat_js @ co_js) 

678 
val problems = 

679 
problems > filter_out_indices bye_js 

680 
> max_potential <= 0 

681 
? filter_out (#liberal o snd) 

682 
in 

683 
solve_any_problem max_potential max_genuine donno false 

684 
problems 

685 
end 

686 
end 

687 
else 

688 
let 

689 
val _ = Library.take (max_genuine, con_ps) 

690 
> List.app (ignore o print_and_check true) 

691 
val max_genuine = max_genuine  length con_ps 

692 
in 

693 
if max_genuine <= 0 orelse not first_time then 

694 
(0, max_genuine, donno) 

695 
else 

696 
let 

697 
val bye_js = sort_distinct int_ord 

698 
(map fst sat_ps @ unsat_js) 

699 
val problems = 

700 
problems > filter_out_indices bye_js 

701 
> filter_out (#liberal o snd) 

702 
in solve_any_problem 0 max_genuine donno false problems end 

703 
end 

704 
end 

705 
 Kodkod.TimedOut unsat_js => 

706 
(update_checked_problems problems unsat_js; raise TimeLimit.TimeOut) 

707 
 Kodkod.Interrupted NONE => 

708 
(checked_problems := NONE; do_interrupted ()) 

709 
 Kodkod.Interrupted (SOME unsat_js) => 

710 
(update_checked_problems problems unsat_js; do_interrupted ()) 

711 
 Kodkod.Error (s, unsat_js) => 

712 
(update_checked_problems problems unsat_js; 

713 
print_v (K ("Kodkod error: " ^ s ^ ".")); 

714 
(max_potential, max_genuine, donno + 1)) 

715 
end 

716 

717 
(* int > int > scope list > int * int * int > int * int * int *) 

718 
fun run_batch j n scopes (max_potential, max_genuine, donno) = 

719 
let 

720 
val _ = 

721 
if null scopes then 

722 
print_m (K "The scope specification is inconsistent.") 

723 
else if verbose then 

724 
pprint (Pretty.chunks 

725 
[Pretty.blk (0, 

726 
pstrs ((if n > 1 then 

727 
"Batch " ^ string_of_int (j + 1) ^ " of " ^ 

728 
signed_string_of_int n ^ ": " 

729 
else 

730 
"") ^ 

731 
"Trying " ^ string_of_int (length scopes) ^ 

732 
" scope" ^ plural_s_for_list scopes ^ ":")), 

733 
Pretty.indent indent_size 

734 
(Pretty.chunks (map2 

735 
(fn j => fn scope => 

736 
Pretty.block ( 

737 
(case pretties_for_scope scope true of 

738 
[] => [Pretty.str "Empty"] 

739 
 pretties => pretties) @ 

740 
[Pretty.str (if j = 1 then "." else ";")])) 

741 
(length scopes downto 1) scopes))]) 

742 
else 

743 
() 

744 
(* scope * bool > rich_problem list * bool 

745 
> rich_problem list * bool *) 

746 
fun add_problem_for_scope (scope as {datatypes, ...}, liberal) 

747 
(problems, donno) = 

748 
(check_deadline (); 

749 
case problem_for_scope liberal scope of 

750 
SOME problem => 

751 
(problems 

752 
> (null problems orelse 

753 
not (Kodkod.problems_equivalent (fst problem) 

754 
(fst (hd problems)))) 

755 
? cons problem, donno) 

756 
 NONE => (problems, donno + 1)) 

757 
val (problems, donno) = 

758 
fold add_problem_for_scope 

759 
(map_product pair scopes 

760 
((if max_genuine > 0 then [false] else []) @ 

761 
(if max_potential > 0 then [true] else []))) 

762 
([], donno) 

763 
val _ = Unsynchronized.change generated_problems (append problems) 

764 
val _ = Unsynchronized.change generated_scopes (append scopes) 

765 
in 

766 
solve_any_problem max_potential max_genuine donno true (rev problems) 

767 
end 

768 

769 
(* rich_problem list > scope > int *) 

770 
fun scope_count (problems : rich_problem list) scope = 

771 
length (filter (scopes_equivalent scope o #scope o snd) problems) 

772 
(* string > string *) 

773 
fun excipit did_so_and_so = 

774 
let 

775 
(* rich_problem list > rich_problem list *) 

776 
val do_filter = 

777 
if !met_potential = max_potential then filter_out (#liberal o snd) 

778 
else I 

779 
val total = length (!scopes) 

780 
val unsat = 

781 
fold (fn scope => 

782 
case scope_count (do_filter (!generated_problems)) scope of 

783 
0 => I 

784 
 n => 

33556
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

785 
scope_count (do_filter (these (!checked_problems))) 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

786 
scope = n 
cba22e2999d5
renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet
parents:
33233
diff
changeset

787 
? Integer.add 1) (!generated_scopes) 0 
33192  788 
in 
789 
"Nitpick " ^ did_so_and_so ^ 

790 
(if is_some (!checked_problems) andalso total > 0 then 

791 
" after checking " ^ 

792 
string_of_int (Int.min (total  1, unsat)) ^ " of " ^ 

793 
string_of_int total ^ " scope" ^ plural_s total 

794 
else 

795 
"") ^ "." 

796 
end 

797 

798 
(* int > int > scope list > int * int * int > Kodkod.outcome *) 

799 
fun run_batches _ _ [] (max_potential, max_genuine, donno) = 

800 
if donno > 0 andalso max_genuine > 0 then 

33233
f9ff11344ec4
added friendly error message when Kodkodi is not available
blanchet
parents:
33232
diff
changeset

801 
(print_m (fn () => excipit "ran into difficulties"); "unknown") 
33192  802 
else if max_genuine = original_max_genuine then 
803 
if max_potential = original_max_potential then 

804 
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none") 

805 
else 

806 
(print_m (K ("Nitpick could not find " ^ 

807 
(if max_genuine = 1 then "a better " ^ word_model ^ "." 

808 
else "any better " ^ word_model ^ "s."))); 

809 
"potential") 

810 
else 

811 
if would_be_genuine then "genuine" else "likely_genuine" 

812 
 run_batches j n (batch :: batches) z = 

813 
let val (z as (_, max_genuine, _)) = run_batch j n batch z in 

814 
run_batches (j + 1) n (if max_genuine > 0 then batches else []) z 

815 
end 

816 

817 
val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns 

818 
iters_assigns bisim_depths mono_Ts nonmono_Ts 

33558
a2db56854b83
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet
parents:
33556
diff
changeset

819 
shallow_dataTs 
33192  820 
val batches = batch_list batch_size (!scopes) 
821 
val outcome_code = 

822 
(run_batches 0 (length batches) batches (max_potential, max_genuine, 0) 

823 
handle Exn.Interrupt => do_interrupted ()) 

824 
handle TimeLimit.TimeOut => 

825 
(print_m (fn () => excipit "ran out of time"); 

826 
if !met_potential > 0 then "potential" else "unknown") 

827 
 Exn.Interrupt => if auto orelse debug then raise Interrupt 

828 
else error (excipit "was interrupted") 

829 
val _ = print_v (fn () => "Total time: " ^ 

830 
signed_string_of_int (Time.toMilliseconds 

831 
(Timer.checkRealTimer timer)) ^ " ms.") 

832 
in (outcome_code, !state_ref) end 

833 
handle Exn.Interrupt => 

834 
if auto orelse #debug params then 

835 
raise Interrupt 

836 
else 

837 
if passed_deadline deadline then 

838 
(priority "Nitpick ran out of time."; ("unknown", state)) 

839 
else 

840 
error "Nitpick was interrupted." 

841 

842 
(* Proof.state > params > bool > term > string * Proof.state *) 

843 
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) 

844 
auto orig_assm_ts orig_t = 

845 
let 

846 
val deadline = Option.map (curry Time.+ (Time.now ())) timeout 

847 
val outcome as (outcome_code, _) = 

848 
time_limit (if debug then NONE else timeout) 

849 
(pick_them_nits_in_term deadline state params auto orig_assm_ts) 

850 
orig_t 

851 
in 

852 
if expect = "" orelse outcome_code = expect then outcome 

853 
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".") 

854 
end 

855 

856 
(* Proof.state > params > thm > int > string * Proof.state *) 

857 
fun pick_nits_in_subgoal state params auto subgoal = 

858 
let 

859 
val ctxt = Proof.context_of state 

860 
val t = state > Proof.get_goal > snd > snd > prop_of 

861 
in 

862 
if Logic.count_prems t = 0 then 

863 
(priority "No subgoal!"; ("none", state)) 

864 
else 

865 
let 

866 
val assms = map term_of (Assumption.all_assms_of ctxt) 

867 
val (t, frees) = Logic.goal_params t subgoal 

868 
in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end 

869 
end 

870 

871 
end; 