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) ;; *)
25 (t Terms.bag * int * t Terms.substitution * int list) list
28 | Timeout of int * t Terms.bag
29 type bag = t Terms.bag * int
31 val empty_state : state
32 val bag_of_state : state -> bag
33 val replace_bag: state -> bag -> state
34 val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
35 val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
36 val forward_infer_step :
38 t Terms.unit_clause ->
52 g_passives:t Terms.unit_clause list ->
53 passives:t Terms.unit_clause list -> szsontology
55 state -> input* input -> szsontology
58 module Paramod (B : Orderings.Blob) = struct
60 module FU = FoUnif.Founif(B)
61 module IDX = Index.Index(B)
62 module Sup = Superposition.Superposition(B)
63 module Utils = FoUtils.Utils(B)
65 module WeightOrderedPassives =
67 type t = B.t Terms.passive_clause
68 let compare = Utils.compare_passive_clauses_weight
71 module AgeOrderedPassives =
73 type t = B.t Terms.passive_clause
74 let compare = Utils.compare_passive_clauses_age
77 module WeightPassiveSet = Set.Make(WeightOrderedPassives)
78 module AgePassiveSet = Set.Make(AgeOrderedPassives)
82 type bag = B.t Terms.bag * int
85 (B.t Terms.bag * int * B.t Terms.substitution * int list) list
88 | Timeout of int * B.t Terms.bag
89 exception Stop of szsontology
93 * Index.Index(B).active_set
94 * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
95 * B.t Terms.unit_clause list
96 * (WeightPassiveSet.t * AgePassiveSet.t)
102 (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty),
104 (WeightPassiveSet.empty,AgePassiveSet.empty)
107 let bag_of_state (bag,n,_,_,_,_) = bag,n
110 let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d
113 let add_passive_clause ?(no_weight=false)
114 (passive_t,passives_w,passives_a) cl =
115 let pcl = if no_weight then (0,cl)
116 else Utils.mk_passive_clause cl in
117 IDX.index_unit_clause passive_t cl,
118 WeightPassiveSet.add pcl passives_w,
119 AgePassiveSet.add pcl passives_a
122 let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
123 let g = if no_weight then (0,g)
124 else Utils.mk_passive_goal g in
125 WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
128 let remove_passive_clause (passive_t,passives_w,passives_a) cl =
129 let passive_t = IDX.remove_unit_clause passive_t (snd cl) in
130 let passives_w = WeightPassiveSet.remove cl passives_w in
131 let passives_a = AgePassiveSet.remove cl passives_a in
132 passive_t,passives_w,passives_a
135 let add_passive_clauses ?(no_weight=false) =
136 List.fold_left (add_passive_clause ~no_weight)
139 let add_passive_goals ?(no_weight=false)
140 (passives_w,passives_a) new_clauses =
141 let new_clauses_w,new_clauses_a =
142 List.fold_left (add_passive_goal ~no_weight)
143 (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
145 (WeightPassiveSet.union new_clauses_w passives_w,
146 AgePassiveSet.union new_clauses_a passives_a)
149 let remove_passive_goal (passives_w,passives_a) cl =
150 let passives_w = WeightPassiveSet.remove cl passives_w in
151 let passives_a = AgePassiveSet.remove cl passives_a in
152 passives_w,passives_a
155 let is_passive_set_empty (_,passives_w,passives_a) =
156 if (WeightPassiveSet.is_empty passives_w) then begin
157 assert (AgePassiveSet.is_empty passives_a); true
159 assert (not (AgePassiveSet.is_empty passives_a)); false
163 let is_passive_g_set_empty (passives_w,passives_a) =
164 if (WeightPassiveSet.is_empty passives_w) then begin
165 assert (AgePassiveSet.is_empty passives_a); true
167 assert (not (AgePassiveSet.is_empty passives_a)); false
171 let passive_set_cardinal (_,passives_w,_)
172 = WeightPassiveSet.cardinal passives_w
175 let g_passive_set_cardinal (passives_w,_)
176 = WeightPassiveSet.cardinal passives_w
179 let passive_empty_set =
180 (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty)
183 let g_passive_empty_set =
184 (WeightPassiveSet.empty,AgePassiveSet.empty)
187 let pick_min_passive ~use_age (_,passives_w,passives_a) =
188 if use_age then AgePassiveSet.min_elt passives_a
189 else WeightPassiveSet.min_elt passives_w
192 let pick_min_g_passive ~use_age (passives_w,passives_a) =
193 if use_age then AgePassiveSet.min_elt passives_a
194 else WeightPassiveSet.min_elt passives_w
197 let mk_clause bag maxvar (t,ty) =
198 let (proof,ty) = B.saturate t ty in
199 let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
200 let bag, c = Terms.add_to_bag c bag in
204 let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
205 let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
206 let initialize_goal (bag,maxvar,actives,passives,_,_) t =
207 let (bag,maxvar), g = mk_goal (bag,maxvar) t in
208 let g_passives = g_passive_empty_set in
209 (* if the goal is not an equation we returns an empty
212 if Terms.is_eq_clause g then add_passive_goal g_passives g
215 (bag,maxvar,actives,passives,[],g_passives)
218 (* TODO : global age over facts and goals (without comparing weights) *)
219 let select ~use_age passives g_passives =
220 if is_passive_set_empty passives then begin
221 if (is_passive_g_set_empty g_passives) then
222 raise (Stop GaveUp) (* we say we are incomplete *)
224 let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
225 (true,g_cl,passives,remove_passive_goal g_passives g_cl)
227 else let cl = pick_min_passive ~use_age:use_age passives in
228 if is_passive_g_set_empty g_passives then
229 (false,cl,remove_passive_clause passives cl,g_passives)
231 let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
232 let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
233 let cmp = if use_age then id1 <= id2
234 else fst cl <= fst g_cl
237 (false,cl,remove_passive_clause passives cl,g_passives)
239 (true,g_cl,passives,remove_passive_goal g_passives g_cl)
242 let backward_infer_step bag maxvar actives passives
243 g_actives g_passives g_current iterno =
244 (* superposition left, simplifications on goals *)
245 debug (lazy "infer_left step...");
246 let bag, maxvar, new_goals =
247 Sup.infer_left bag maxvar g_current actives
249 debug (lazy "Performed infer_left step");
250 let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
251 bag, maxvar, actives, passives, g_current::g_actives,
252 (add_passive_goals g_passives new_goals)
255 let forward_infer_step
256 ((bag,maxvar,actives,passives,g_actives,g_passives) as s)
262 * A' = demod [e'] A *
265 * new = supright e'' A'' *
266 * new'= demod A'' new *
268 debug (lazy "Forward infer step...");
269 debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
270 let id,_,_,_ = current in
271 let _ = Terms.get_from_bag id bag in
273 match Sup.keep_simplified current actives bag maxvar
276 | bag,Some (current,actives) ->
277 debug (lazy "simplified...");
278 let bag, maxvar, actives, new_clauses =
279 Sup.infer_right bag maxvar current actives
281 debug (lazy "Demodulating goals with actives...");
282 (* keep goals demodulated w.r.t. actives and check if solved *)
287 Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
290 | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
293 let ctable = IDX.index_unit_clause IDX.DT.empty current in
294 let bag, maxvar, new_goals =
296 (fun (bag,m,acc) g ->
297 let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
299 (bag,maxvar,[]) g_actives
301 let bag = Terms.replace_in_bag (current,false,iterno) bag in
302 (* prerr_endline (Pp.pp_bag bag); *)
303 bag, maxvar, actives,
304 add_passive_clauses passives new_clauses, g_actives,
305 add_passive_goals g_passives new_goals
308 let debug_status (_,_,actives,passives,g_actives,g_passives) =
310 ((Printf.sprintf "Number of active goals : %d\n"
311 (List.length g_actives)) ^
312 (Printf.sprintf "Number of passive goals : %d\n"
313 (g_passive_set_cardinal g_passives)) ^
314 (Printf.sprintf "Number of actives : %d\n"
315 (List.length (fst actives))) ^
316 (Printf.sprintf "Number of passives : %d\n"
317 (passive_set_cardinal passives)))
321 (* we just check if any of the active goals is subsumed by a
322 passive clause, or if any of the passive goal is subsumed
323 by an active or passive clause *)
324 let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
325 debug (lazy("Last chance " ^ string_of_float
326 (Unix.gettimeofday())));
327 let active_t = snd actives in
328 let passive_t,wset,_ = passives in
331 ("Passive set :" ^ (String.concat ";\n"
332 (List.map (fun _,cl -> Pp.pp_unit_clause cl)
333 (WeightPassiveSet.elements wset))))) in
334 let wset = IDX.elems passive_t in
337 ("Passive table :" ^(String.concat ";\n"
338 (List.map (fun _,cl -> Pp.pp_unit_clause cl)
339 (IDX.ClauseSet.elements wset))))) in
341 WeightPassiveSet.fold
343 if List.exists (Sup.are_alpha_eq x) g_actives then acc
351 (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
357 (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
358 (g_actives@g_passives));
359 raise (Stop (Timeout (maxvar,bag)))
361 let check_timeout = function
363 | Some timeout -> Unix.gettimeofday () > timeout
365 let rec given_clause ~useage
366 bag maxvar iterno weight_picks max_steps timeout
367 actives passives g_actives g_passives
369 let iterno = iterno + 1 in
370 if iterno = max_steps || check_timeout timeout then
371 last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
373 let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
374 let weight_picks = if use_age then 0 else weight_picks+1
377 let rec aux_select bag
378 (passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
380 let backward,(weight,current),passives,g_passives =
381 select ~use_age passives g_passives
383 if use_age && weight > monster then
384 let bag,cl = Terms.add_to_bag current bag in
386 aux_select bag passives (add_passive_goal g_passives cl)
388 aux_select bag (add_passive_clause passives cl) g_passives
390 let bag = Terms.replace_in_bag (current,false,iterno) bag in
392 let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
395 ~no_demod:false maxvar (snd actives) bag g_actives current
397 | None -> aux_select bag passives g_passives
398 | Some (bag,g_current) ->
399 backward_infer_step bag maxvar actives passives
400 g_actives g_passives g_current iterno
402 let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current))
404 if Sup.orphan_murder bag (fst actives) current then
405 let _ = debug (lazy "Orphan murdered") in
406 let bag = Terms.replace_in_bag (current,true,iterno) bag in
407 aux_select bag passives g_passives
409 let s = bag,maxvar,actives,passives,g_actives,g_passives in
410 let s1 = forward_infer_step s current iterno
412 if s == s1 then aux_select bag passives g_passives
415 (*prerr_endline "Active table :";
416 (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
419 let (bag,maxvar,actives,passives,g_actives,g_passives) as status =
420 aux_select bag passives g_passives
422 debug (debug_status status);
424 bag maxvar iterno weight_picks max_steps timeout
425 actives passives g_actives g_passives
428 (* similar to given_clause, but it merely works on goals,
429 in parallel, at each iteration *)
430 let rec goal_narrowing iterno max_steps timeout status
432 debug (debug_status status);
433 let iterno = iterno + 1 in
434 if iterno = max_steps || check_timeout timeout then
437 let _,_,_,_,_,g_passives = status in
438 let passive_goals = WeightPassiveSet.elements (fst g_passives) in
442 let bag,maxvar,actives,passives,g_actives,g_passives = acc in
444 remove_passive_goal g_passives g in
445 let current = snd g in
447 debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
451 ~no_demod:false maxvar (snd actives) bag g_actives current
454 | Some (bag,g_current) ->
456 debug (lazy("Demodulated goal : "
457 ^ Pp.pp_unit_clause g_current))
459 backward_infer_step bag maxvar actives passives
460 g_actives g_passives g_current iterno)
463 goal_narrowing iterno max_steps timeout newstatus
465 let compute_result bag i subst =
467 let rec traverse ongoal (accg,acce) i =
468 match Terms.get_from_bag i bag with
469 | (id,_,_,Terms.Exact _),_,_ ->
470 if ongoal then [i],acce else
471 if (List.mem i acce) then accg,acce else accg,acce@[i]
472 | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
473 if (not ongoal) && (List.mem i acce) then accg,acce
476 traverse false (traverse ongoal (accg,acce) i1) i2
478 if ongoal then i::accg,acce else accg,i::acce
480 let gsteps,esteps = traverse true ([],[]) i in
481 (List.rev esteps)@gsteps
483 debug (lazy ("steps: " ^ (string_of_int (List.length l))));
487 let (cl,_,_) = Terms.get_from_bag i bag in
488 max acc (Order.compute_unit_clause_weight cl)) 0 l in
489 debug (lazy ("Max weight : " ^ (string_of_int max_w)));
490 (* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
491 Terms.get_from_bag id bag in
494 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
495 id it (Order.compute_unit_clause_weight cl)
496 (Pp.pp_proof_step proof))
499 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
500 id it (Order.compute_unit_clause_weight cl)
501 (Pp.pp_proof_step proof))) l;*)
502 debug (lazy ("Proof:" ^
506 let cl,_,_ = Terms.get_from_bag x bag in
507 Pp.pp_unit_clause cl) l))));
508 Unsatisfiable [ bag, i, subst, l ]
510 let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
511 let _initial_timestamp = Unix.gettimeofday () in
513 add_passive_clauses ~no_weight:true passive_empty_set passives
516 add_passive_goals ~no_weight:true g_passive_empty_set g_passives
518 let g_actives = [] in
519 let actives = [], IDX.DT.empty in
521 given_clause ~useage ~noinfer:false
522 bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
524 | Sup.Success (bag, _, (i,_,_,_),subst) ->
525 compute_result bag i subst
526 | Stop (Unsatisfiable _) -> Error "solution found!"
530 let fast_eq_check s goal =
531 let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
532 if is_passive_g_set_empty g_passives then Error "not an equation"
535 goal_narrowing 0 2 None s
537 | Sup.Success (bag, _, (i,_,_,_),subst) ->
538 compute_result bag i subst
539 | Stop (Unsatisfiable _) -> Error "solution found!"