2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
14 let debug s = prerr_endline (Lazy.force s) ;;
23 | Unsatisfiable of (t Terms.bag * int * int list) list
26 | Timeout of int * t Terms.bag
32 t Terms.foterm * (t Terms.foterm list * t Terms.foterm list) ->
33 (t Terms.foterm * (t Terms.foterm list * t Terms.foterm list)) list -> szsontology
36 module Paramod (B : Orderings.Blob) = struct
39 | Unsatisfiable of (B.t Terms.bag * int * int list) list
42 | Timeout of int * B.t Terms.bag
43 exception Stop of szsontology
44 type bag = B.t Terms.bag * int
46 module FU = FoUnif.FoUnif(B)
47 module IDX = Index.Index(B)
48 module Sup = Superposition.Superposition(B)
49 module Utils = FoUtils.Utils(B)
51 module Clauses = Clauses.Clauses(B)
52 module WeightOrderedPassives =
54 type t = B.t Terms.passive_clause
55 let compare = Clauses.compare_passive_clauses_weight
58 module AgeOrderedPassives =
60 type t = B.t Terms.passive_clause
61 let compare = Clauses.compare_passive_clauses_age
64 module WeightPassiveSet = Set.Make(WeightOrderedPassives)
65 module AgePassiveSet = Set.Make(AgeOrderedPassives)
67 let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
68 let (w,cl) = Clauses.mk_passive_clause cl in
69 (* let cl = (w+bonus_weight,cl) in *)
70 let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in
71 WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
74 let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
75 let (w,g) = Clauses.mk_passive_goal g in
76 (* let g = (w+bonus_weight,g) in *)
77 let g = if bonus_weight = 0 then (w,g) else (0,g) in
78 WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
81 let remove_passive_clause (passives_w,passives_a) cl =
82 let passives_w = WeightPassiveSet.remove cl passives_w in
83 let passives_a = AgePassiveSet.remove cl passives_a in
87 let add_passive_clauses ?(bonus_weight=0)
88 (passives_w,passives_a) new_clauses =
89 let new_clauses_w,new_clauses_a =
90 List.fold_left (add_passive_clause ~bonus_weight)
91 (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
93 (WeightPassiveSet.union new_clauses_w passives_w,
94 AgePassiveSet.union new_clauses_a passives_a)
97 let add_passive_goals ?(bonus_weight=0)
98 (passives_w,passives_a) new_clauses =
99 let new_clauses_w,new_clauses_a =
100 List.fold_left (add_passive_goal ~bonus_weight)
101 (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
103 (WeightPassiveSet.union new_clauses_w passives_w,
104 AgePassiveSet.union new_clauses_a passives_a)
107 let is_passive_set_empty (passives_w,passives_a) =
108 if (WeightPassiveSet.is_empty passives_w) then begin
109 assert (AgePassiveSet.is_empty passives_a); true
111 assert (not (AgePassiveSet.is_empty passives_a)); false
115 let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w
117 let passive_empty_set =
118 (WeightPassiveSet.empty,AgePassiveSet.empty)
121 let pick_min_passive ~use_age (passives_w,passives_a) =
122 if use_age then AgePassiveSet.min_elt passives_a
123 else WeightPassiveSet.min_elt passives_w
126 (* TODO : global age over facts and goals (without comparing weights) *)
127 let select ~use_age passives g_passives =
128 if is_passive_set_empty passives then begin
129 if (is_passive_set_empty g_passives) then
130 raise (Stop GaveUp) (* we say we are incomplete *)
132 let g_cl = pick_min_passive ~use_age:use_age g_passives in
133 (true,g_cl,passives,remove_passive_clause g_passives g_cl)
135 else let cl = pick_min_passive ~use_age:use_age passives in
136 if is_passive_set_empty g_passives then
137 (false,cl,remove_passive_clause passives cl,g_passives)
139 let g_cl = pick_min_passive ~use_age:use_age g_passives in
140 let (id1,_,_,_,_),(id2,_,_,_,_) = snd cl, snd g_cl in
141 let cmp = if use_age then id1 <= id2
142 else fst cl <= fst g_cl
145 (false,cl,remove_passive_clause passives cl,g_passives)
147 (true,g_cl,passives,remove_passive_clause g_passives g_cl)
150 let backward_infer_step bag maxvar actives passives
151 g_actives g_passives g_current iterno =
152 (* superposition left, simplifications on goals *)
153 debug (lazy "infer_left step...");
154 let bag, maxvar, new_goals =
155 Sup.infer_left bag maxvar g_current actives
157 debug (lazy "Performed infer_left step");
158 let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
159 bag, maxvar, actives, passives, g_current::g_actives,
160 (add_passive_goals g_passives new_goals)
163 let forward_infer_step bag maxvar actives passives g_actives
164 g_passives current iterno =
169 * A' = demod [e'] A *
172 * new = supright e'' A'' *
173 * new'= demod A'' new *
175 debug (lazy "Forward infer step...");
176 debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
177 let bag, maxvar, actives, new_clauses =
178 Sup.infer_right bag maxvar current actives
180 debug (lazy "Demodulating goals with actives...");
181 (* keep goals demodulated w.r.t. actives and check if solved *)
186 Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
189 | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
192 let ctable = IDX.index_clause IDX.DT.empty current in
193 let bag, maxvar, new_goals =
195 (fun (bag,m,acc) g ->
196 let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
198 (bag,maxvar,[]) g_actives
200 let bag = Terms.replace_in_bag (current,false,iterno) bag in
201 bag, maxvar, actives,
202 add_passive_clauses passives new_clauses, g_actives,
203 add_passive_goals g_passives new_goals
206 let rec given_clause ~useage ~noinfer
207 bag maxvar iterno weight_picks max_steps timeout
208 actives passives g_actives g_passives
210 let iterno = iterno + 1 in
211 if iterno = max_steps then raise (Stop (Timeout (maxvar,bag)));
212 (* timeout check: gettimeofday called only if timeout set *)
213 if timeout <> None &&
215 | None -> assert false
216 | Some timeout -> Unix.gettimeofday () > timeout) then
220 (lazy("Last chance: all is indexed " ^ string_of_float
221 (Unix.gettimeofday())));
222 let maxgoals = 100 in
223 ignore(List.fold_left
226 ignore(Sup.simplify_goal ~no_demod:true
227 maxvar (snd actives) bag acc x)
232 raise (Stop (Timeout (maxvar,bag)))
234 else if false then (* activates last chance strategy *)
236 debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday())));
237 given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps
238 (Some (Unix.gettimeofday () +. 20.))
239 actives passives g_actives g_passives;
240 raise (Stop (Timeout (maxvar,bag)));
242 else raise (Stop (Timeout (maxvar,bag)));
244 let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
245 let weight_picks = if use_age then 0 else weight_picks+1
248 let rec aux_select bag passives g_passives =
249 let backward,(weight,current),passives,g_passives =
250 select ~use_age passives g_passives
252 if use_age && weight > monster then
253 let bag,cl = Terms.add_to_bag current bag in
255 aux_select bag passives (add_passive_clause g_passives cl)
257 aux_select bag (add_passive_clause passives cl) g_passives
259 let bag = Terms.replace_in_bag (current,false,iterno) bag in
261 let _ = debug (lazy("Selected goal : " ^ Pp.pp_clause current)) in
264 if weight > monster then None else Some (bag,current)
267 ~no_demod:false maxvar (snd actives) bag g_actives current
269 | None -> aux_select bag passives g_passives
270 | Some (bag,g_current) ->
272 let g_actives = g_current :: g_actives in
273 bag,maxvar,actives,passives,g_actives,g_passives
275 backward_infer_step bag maxvar actives passives
276 g_actives g_passives g_current iterno
278 let _ = debug (lazy("Selected fact : " ^ Pp.pp_clause current)) in
279 (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*)
282 if weight > monster then bag,None
283 else bag, Some (current,actives)
284 else if Sup.orphan_murder bag (fst actives) current then
285 let _ = debug (lazy "Orphan murdered") in
286 let bag = Terms.replace_in_bag (current,true,iterno) bag in
288 else Sup.keep_simplified current actives bag maxvar
290 (*match Sup.one_pass_simplification current actives bag maxvar with*)
291 | bag,None -> aux_select bag passives g_passives
292 | bag,Some (current,actives) ->
293 (* if is_orphan then prerr_endline
294 ("WRONG discarded: " ^ (Pp.pp_unit_clause current));
296 prerr_endline (Pp.pp_unit_clause x))
299 (* List.iter (fun (id,_,_,_) -> let (cl,d) =
300 Terms.M.find id bag in
301 if d then prerr_endline
302 ("WRONG discarded: " ^ (Pp.pp_unit_clause cl)))
303 (current::fst actives);*)
306 current::fst actives,
307 IDX.index_clause (snd actives) current
309 bag,maxvar,actives,passives,g_actives,g_passives
311 forward_infer_step bag maxvar actives passives
312 g_actives g_passives current iterno
316 (*prerr_endline "Active table :";
317 (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
319 let bag,maxvar,actives,passives,g_actives,g_passives =
320 aux_select bag passives g_passives
323 (lazy(Printf.sprintf "Number of active goals : %d"
324 (List.length g_actives)));
326 (lazy(Printf.sprintf "Number of passive goals : %d"
327 (passive_set_cardinal g_passives)));
329 (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives))));
331 (lazy(Printf.sprintf "Number of passives : %d"
332 (passive_set_cardinal passives)));
333 given_clause ~useage ~noinfer
334 bag maxvar iterno weight_picks max_steps timeout
335 actives passives g_actives g_passives
338 let paramod ~useage ~max_steps ~print_problem ?timeout goal hypotheses =
339 let initial_timestamp = Unix.gettimeofday () in
340 let bag = Terms.empty_bag in
342 let build_clause (bag,maxvar,l) (t,(nlit,plit)) =
343 let c,maxvar = Clauses.mk_clause maxvar nlit plit t in
344 let bag,c = Terms.add_to_bag c bag in
347 let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
348 let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
349 let goal = match goals with | [g] -> g | _ -> assert false in
351 add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses
354 add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal
356 let g_actives = [] in
357 let actives = [], IDX.DT.empty in
358 if print_problem then begin
359 prerr_endline "Facts:";
360 List.iter (fun x -> prerr_endline (" " ^ Pp.pp_clause x)) hypotheses;
361 prerr_endline "Goal:";
362 prerr_endline (" " ^ Pp.pp_clause goal);
365 given_clause ~useage ~noinfer:false
366 bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
368 | Sup.Success (bag, _, (i,_,_,_,_)) ->
370 let rec traverse ongoal (accg,acce) i =
371 match Terms.get_from_bag i bag with
372 | (id,_,_,_,Terms.Exact _),_,_ ->
373 if ongoal then [i],acce else
374 if (List.mem i acce) then accg,acce else accg,acce@[i]
375 | (_,_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
376 if (not ongoal) && (List.mem i acce) then accg,acce
379 traverse false (traverse ongoal (accg,acce) i1) i2
381 if ongoal then i::accg,acce else accg,i::acce
383 let gsteps,esteps = traverse true ([],[]) i in
384 (List.rev esteps)@gsteps
386 let max_w = List.fold_left (fun acc i ->
387 let (cl,_,_) = Terms.get_from_bag i bag in
388 max acc (Order.compute_clause_weight cl)) 0 l in
389 prerr_endline "Statistics :";
390 prerr_endline ("Max weight : " ^ (string_of_int max_w));
391 (* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
392 Terms.get_from_bag id bag in
395 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
396 id it (Order.compute_unit_clause_weight cl)
397 (Pp.pp_proof_step proof))
400 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
401 id it (Order.compute_unit_clause_weight cl)
402 (Pp.pp_proof_step proof))) l;*)
404 (Printf.sprintf "Found proof, %fs"
405 (Unix.gettimeofday() -. initial_timestamp));
407 prerr_endline "Proof:";
409 prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
411 Unsatisfiable [ bag, i, l ]
412 | Stop (Unsatisfiable _) -> Error "stop bug solution found!"