From 646da3fc52fa905a67959cfa1191eb5c96edaef1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 2 Dec 2009 10:01:06 +0000 Subject: [PATCH] Passive equations have their own index (not passive goals). New, simple version of "last chance" (yet to be improved). Added a narrowing function the merely works on goals, in parallel. --- .../components/ng_paramodulation/paramod.ml | 435 +++++++++++------- .../components/ng_paramodulation/paramod.mli | 10 + 2 files changed, 271 insertions(+), 174 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 6f76e2ad4..3af1a38e4 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -12,7 +12,7 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) let debug s = prerr_endline (Lazy.force s) ;; -let debug _ = ();; +(* let debug _ = ();; *) let monster = 100;; @@ -20,14 +20,16 @@ module type Paramod = sig type t type input - type state type szsontology = | Unsatisfiable of (t Terms.bag * int * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag type bag = t Terms.bag * int + type state val empty_state : state + val bag_of_state : state -> bag + val replace_bag: state -> bag -> state val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause val forward_infer_step : @@ -35,6 +37,12 @@ module type Paramod = t Terms.unit_clause -> int -> state + val goal_narrowing : + int + -> int + -> float option + -> state + -> state val paramod : useage:bool -> max_steps:int -> @@ -42,6 +50,8 @@ module type Paramod = bag -> g_passives:t Terms.unit_clause list -> passives:t Terms.unit_clause list -> szsontology + val fast_eq_check : + state -> input* input -> szsontology end module Paramod (B : Orderings.Blob) = struct @@ -68,34 +78,43 @@ module Paramod (B : Orderings.Blob) = struct type t = B.t type input = B.input - type state = - B.t Terms.bag - * int - * Index.Index(B).active_set - * (WeightPassiveSet.t * AgePassiveSet.t) - * B.t Terms.unit_clause list - * (WeightPassiveSet.t * AgePassiveSet.t) + type bag = B.t Terms.bag * int type szsontology = | Unsatisfiable of (B.t Terms.bag * int * int list) list | GaveUp | Error of string | Timeout of int * B.t Terms.bag exception Stop of szsontology - type bag = B.t Terms.bag * int + type state = + t Terms.bag + * int + * Index.Index(B).active_set + * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t) + * B.t Terms.unit_clause list + * (WeightPassiveSet.t * AgePassiveSet.t) let empty_state = Terms.empty_bag, 0, ([],IDX.DT.empty), - (WeightPassiveSet.empty,AgePassiveSet.empty), + (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty), [], (WeightPassiveSet.empty,AgePassiveSet.empty) -;; + ;; + + let bag_of_state (bag,n,_,_,_,_) = bag,n + ;; + + let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d + ;; - let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl = - let cl = if no_weight then (0,cl) + let add_passive_clause ?(no_weight=false) + (passive_t,passives_w,passives_a) cl = + let pcl = if no_weight then (0,cl) else Utils.mk_passive_clause cl in - WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a + IDX.index_unit_clause passive_t cl, + WeightPassiveSet.add pcl passives_w, + AgePassiveSet.add pcl passives_a ;; let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g = @@ -104,20 +123,15 @@ module Paramod (B : Orderings.Blob) = struct WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a ;; - let remove_passive_clause (passives_w,passives_a) cl = + let remove_passive_clause (passive_t,passives_w,passives_a) cl = + let passive_t = IDX.remove_unit_clause passive_t (snd cl) in let passives_w = WeightPassiveSet.remove cl passives_w in let passives_a = AgePassiveSet.remove cl passives_a in - passives_w,passives_a + passive_t,passives_w,passives_a ;; - let add_passive_clauses ?(no_weight=false) - (passives_w,passives_a) new_clauses = - let new_clauses_w,new_clauses_a = - List.fold_left (add_passive_clause ~no_weight) - (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses - in - (WeightPassiveSet.union new_clauses_w passives_w, - AgePassiveSet.union new_clauses_a passives_a) + let add_passive_clauses ?(no_weight=false) = + List.fold_left (add_passive_clause ~no_weight) ;; let add_passive_goals ?(no_weight=false) @@ -130,7 +144,13 @@ module Paramod (B : Orderings.Blob) = struct AgePassiveSet.union new_clauses_a passives_a) ;; - let is_passive_set_empty (passives_w,passives_a) = + let remove_passive_goal (passives_w,passives_a) cl = + let passives_w = WeightPassiveSet.remove cl passives_w in + let passives_a = AgePassiveSet.remove cl passives_a in + passives_w,passives_a + ;; + + let is_passive_set_empty (_,passives_w,passives_a) = if (WeightPassiveSet.is_empty passives_w) then begin assert (AgePassiveSet.is_empty passives_a); true end else begin @@ -138,13 +158,36 @@ module Paramod (B : Orderings.Blob) = struct end ;; - let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w - + let is_passive_g_set_empty (passives_w,passives_a) = + if (WeightPassiveSet.is_empty passives_w) then begin + assert (AgePassiveSet.is_empty passives_a); true + end else begin + assert (not (AgePassiveSet.is_empty passives_a)); false + end + ;; + + let passive_set_cardinal (_,passives_w,_) + = WeightPassiveSet.cardinal passives_w + ;; + + let g_passive_set_cardinal (passives_w,_) + = WeightPassiveSet.cardinal passives_w + ;; + let passive_empty_set = + (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty) + ;; + + let g_passive_empty_set = (WeightPassiveSet.empty,AgePassiveSet.empty) ;; - let pick_min_passive ~use_age (passives_w,passives_a) = + let pick_min_passive ~use_age (_,passives_w,passives_a) = + if use_age then AgePassiveSet.min_elt passives_a + else WeightPassiveSet.min_elt passives_w + ;; + + let pick_min_g_passive ~use_age (passives_w,passives_a) = if use_age then AgePassiveSet.min_elt passives_a else WeightPassiveSet.min_elt passives_w ;; @@ -158,21 +201,27 @@ module Paramod (B : Orderings.Blob) = struct let mk_passive (bag,maxvar) = mk_clause bag maxvar;; let mk_goal (bag,maxvar) = mk_clause bag maxvar;; + let initialize_goal (bag,maxvar,actives,passives,_,_) t = + let (bag,maxvar), g = mk_goal (bag,maxvar) t in + let g_passives = g_passive_empty_set in + let g_passives = add_passive_goal g_passives g in + (bag,maxvar,actives,passives,[],g_passives) + (* TODO : global age over facts and goals (without comparing weights) *) let select ~use_age passives g_passives = if is_passive_set_empty passives then begin - if (is_passive_set_empty g_passives) then + if (is_passive_g_set_empty g_passives) then raise (Stop GaveUp) (* we say we are incomplete *) else - let g_cl = pick_min_passive ~use_age:use_age g_passives in - (true,g_cl,passives,remove_passive_clause g_passives g_cl) + let g_cl = pick_min_g_passive ~use_age:use_age g_passives in + (true,g_cl,passives,remove_passive_goal g_passives g_cl) end else let cl = pick_min_passive ~use_age:use_age passives in - if is_passive_set_empty g_passives then + if is_passive_g_set_empty g_passives then (false,cl,remove_passive_clause passives cl,g_passives) else - let g_cl = pick_min_passive ~use_age:use_age g_passives in + let g_cl = pick_min_g_passive ~use_age:use_age g_passives in let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in let cmp = if use_age then id1 <= id2 else fst cl <= fst g_cl @@ -180,7 +229,7 @@ module Paramod (B : Orderings.Blob) = struct if cmp then (false,cl,remove_passive_clause passives cl,g_passives) else - (true,g_cl,passives,remove_passive_clause g_passives g_cl) + (true,g_cl,passives,remove_passive_goal g_passives g_cl) ;; let backward_infer_step bag maxvar actives passives @@ -196,7 +245,8 @@ module Paramod (B : Orderings.Blob) = struct (add_passive_goals g_passives new_goals) ;; - let forward_infer_step (bag,maxvar,actives,passives,g_actives,g_passives) + let forward_infer_step + ((bag,maxvar,actives,passives,g_actives,g_passives) as s) current iterno = (* forward step *) @@ -210,6 +260,14 @@ module Paramod (B : Orderings.Blob) = struct * P' = P + new' *) debug (lazy "Forward infer step..."); debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); + let id,_,_,_ = current in + let _ = Terms.get_from_bag id bag in + + match Sup.keep_simplified current actives bag maxvar + with + | _,None -> s + | bag,Some (current,actives) -> + debug (lazy "simplified..."); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in @@ -225,7 +283,7 @@ module Paramod (B : Orderings.Blob) = struct | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc) (bag,[]) g_actives in - let ctable = IDX.index_unit_clause maxvar IDX.DT.empty current in + let ctable = IDX.index_unit_clause IDX.DT.empty current in let bag, maxvar, new_goals = List.fold_left (fun (bag,m,acc) g -> @@ -239,57 +297,75 @@ module Paramod (B : Orderings.Blob) = struct add_passive_clauses passives new_clauses, g_actives, add_passive_goals g_passives new_goals ;; + + let debug_status (_,_,actives,passives,g_actives,g_passives) = + lazy + ((Printf.sprintf "Number of active goals : %d\n" + (List.length g_actives)) ^ + (Printf.sprintf "Number of passive goals : %d\n" + (g_passive_set_cardinal g_passives)) ^ + (Printf.sprintf "Number of actives : %d\n" + (List.length (fst actives))) ^ + (Printf.sprintf "Number of passives : %d\n" + (passive_set_cardinal passives))) + ;; + + + (* we just check if any of the active goals is subsumed by a + passive clause, or if any of the passive goal is subsumed + by an active or passive clause *) + let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) = + debug (lazy("Last chance " ^ string_of_float + (Unix.gettimeofday()))); + let active_t = snd actives in + let passive_t,_,_ = passives in + let g_passives = + WeightPassiveSet.fold + (fun (_,x) acc -> + if List.exists (Sup.are_alpha_eq x) g_actives then acc + else x::acc) + (fst g_passives) [] + in + ignore + (List.iter + (fun x -> + ignore + (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x)) + g_passives); + ignore + (List.iter + (fun x -> + ignore + (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x)) + (g_actives@g_passives)); + raise (Stop (Timeout (maxvar,bag))) + + let check_timeout = function + | None -> false + | Some timeout -> Unix.gettimeofday () > timeout - let rec given_clause ~useage ~noinfer + let rec given_clause ~useage bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives = let iterno = iterno + 1 in - if iterno = max_steps then raise (Stop (Timeout (maxvar,bag))); - (* timeout check: gettimeofday called only if timeout set *) - if timeout <> None && - (match timeout with - | None -> assert false - | Some timeout -> Unix.gettimeofday () > timeout) then - if noinfer then - begin - debug - (lazy("Last chance: all is indexed " ^ string_of_float - (Unix.gettimeofday()))); - let maxgoals = 100 in - ignore(List.fold_left - (fun (acc,i) x -> - if i < maxgoals then - ignore(Sup.simplify_goal ~no_demod:true - maxvar (snd actives) bag acc x) - else - (); - x::acc,i+1) - ([],0) g_actives); - raise (Stop (Timeout (maxvar,bag))) - end - else if false then (* activates last chance strategy *) - begin - debug (lazy("Last chance: "^string_of_float (Unix.gettimeofday()))); - given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps - (Some (Unix.gettimeofday () +. 20.)) - actives passives g_actives g_passives; - raise (Stop (Timeout (maxvar,bag))); - end - else raise (Stop (Timeout (maxvar,bag))); - + if iterno = max_steps || check_timeout timeout then + last_chance (bag,maxvar,actives,passives,g_actives,g_passives) + else let use_age = useage && (weight_picks = (iterno / 6 + 1)) in let weight_picks = if use_age then 0 else weight_picks+1 in - let rec aux_select bag passives g_passives = + let rec aux_select bag + (passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t) + g_passives = let backward,(weight,current),passives,g_passives = select ~use_age passives g_passives in if use_age && weight > monster then let bag,cl = Terms.add_to_bag current bag in if backward then - aux_select bag passives (add_passive_clause g_passives cl) + aux_select bag passives (add_passive_goal g_passives cl) else aux_select bag (add_passive_clause passives cl) g_passives else @@ -297,120 +373,103 @@ module Paramod (B : Orderings.Blob) = struct if backward then let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in match - if noinfer then - if weight > monster then None else Some (bag,current) - else - Sup.simplify_goal - ~no_demod:false maxvar (snd actives) bag g_actives current + Sup.simplify_goal + ~no_demod:false maxvar (snd actives) bag g_actives current with - | None -> aux_select bag passives g_passives - | Some (bag,g_current) -> - if noinfer then - let g_actives = g_current :: g_actives in - bag,maxvar,actives,passives,g_actives,g_passives - else - backward_infer_step bag maxvar actives passives - g_actives g_passives g_current iterno + | None -> aux_select bag passives g_passives + | Some (bag,g_current) -> + backward_infer_step bag maxvar actives passives + g_actives g_passives g_current iterno else - let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current)) in - (*let is_orphan = Sup.orphan_murder bag (fst actives) current in*) - match - if noinfer then - if weight > monster then bag,None - else bag, Some (current,actives) - else if Sup.orphan_murder bag (fst actives) current then + let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current)) + in + if Sup.orphan_murder bag (fst actives) current then let _ = debug (lazy "Orphan murdered") in let bag = Terms.replace_in_bag (current,true,iterno) bag in - bag, None - else Sup.keep_simplified current actives bag maxvar - with - (*match Sup.one_pass_simplification current actives bag maxvar with*) - | bag,None -> aux_select bag passives g_passives - | bag,Some (current,actives) -> -(* if is_orphan then prerr_endline - ("WRONG discarded: " ^ (Pp.pp_unit_clause current)); - List.iter (fun x -> - prerr_endline (Pp.pp_unit_clause x)) - (fst actives);*) - -(* List.iter (fun (id,_,_,_) -> let (cl,d) = - Terms.M.find id bag in - if d then prerr_endline - ("WRONG discarded: " ^ (Pp.pp_unit_clause cl))) - (current::fst actives);*) - if noinfer then - let actives = - current::fst actives, - IDX.index_unit_clause maxvar (snd actives) current - in - bag,maxvar,actives,passives,g_actives,g_passives - else - forward_infer_step - (bag,maxvar,actives,passives,g_actives,g_passives) - current iterno + aux_select bag passives g_passives + else + let s = bag,maxvar,actives,passives,g_actives,g_passives in + let s1 = forward_infer_step s current iterno + in + if s == s1 then aux_select bag passives g_passives + else s1 in - - (*prerr_endline "Active table :"; (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x)) (fst actives)); *) - let bag,maxvar,actives,passives,g_actives,g_passives = + let (bag,maxvar,actives,passives,g_actives,g_passives) as status = aux_select bag passives g_passives in - debug - (lazy(Printf.sprintf "Number of active goals : %d" - (List.length g_actives))); - debug - (lazy(Printf.sprintf "Number of passive goals : %d" - (passive_set_cardinal g_passives))); - debug - (lazy(Printf.sprintf "Number of actives : %d" (List.length (fst actives)))); - debug - (lazy(Printf.sprintf "Number of passives : %d" - (passive_set_cardinal passives))); - given_clause ~useage ~noinfer + debug (debug_status status); + given_clause ~useage bag maxvar iterno weight_picks max_steps timeout actives passives g_actives g_passives ;; - let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = - let _initial_timestamp = Unix.gettimeofday () in - let passives = - add_passive_clauses ~no_weight:true passive_empty_set passives - in - let g_passives = - add_passive_goals ~no_weight:true passive_empty_set g_passives + (* similar to given_clause, but it merely works on goals, + in parallel, at each iteration *) + let rec goal_narrowing iterno max_steps timeout status + = + debug (debug_status status); + let iterno = iterno + 1 in + if iterno = max_steps || check_timeout timeout then + last_chance status + else + let _,_,_,_,_,g_passives = status in + let passive_goals = WeightPassiveSet.elements (fst g_passives) in + let newstatus = + List.fold_left + (fun acc g -> + let bag,maxvar,actives,passives,g_actives,g_passives = acc in + let g_passives = + remove_passive_goal g_passives g in + let current = snd g in + let _ = + debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) + in + match + Sup.simplify_goal + ~no_demod:false maxvar (snd actives) bag g_actives current + with + | None -> acc + | Some (bag,g_current) -> + let _ = + debug (lazy("Demodulated goal : " + ^ Pp.pp_unit_clause g_current)) + in + backward_infer_step bag maxvar actives passives + g_actives g_passives g_current iterno) + status passive_goals in - let g_actives = [] in - let actives = [], IDX.DT.empty in - try - given_clause ~useage ~noinfer:false - bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives - with - | Sup.Success (bag, _, (i,_,_,_)) -> - let l = - let rec traverse ongoal (accg,acce) i = - match Terms.get_from_bag i bag with - | (id,_,_,Terms.Exact _),_,_ -> - if ongoal then [i],acce else - if (List.mem i acce) then accg,acce else accg,acce@[i] - | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ -> - if (not ongoal) && (List.mem i acce) then accg,acce - else - let accg,acce = - traverse false (traverse ongoal (accg,acce) i1) i2 - in - if ongoal then i::accg,acce else accg,i::acce - in - let gsteps,esteps = traverse true ([],[]) i in - (List.rev esteps)@gsteps + goal_narrowing iterno max_steps timeout newstatus + + let compute_result bag i = + let l = + let rec traverse ongoal (accg,acce) i = + match Terms.get_from_bag i bag with + | (id,_,_,Terms.Exact _),_,_ -> + if ongoal then [i],acce else + if (List.mem i acce) then accg,acce else accg,acce@[i] + | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ -> + if (not ongoal) && (List.mem i acce) then accg,acce + else + let accg,acce = + traverse false (traverse ongoal (accg,acce) i1) i2 + in + if ongoal then i::accg,acce else accg,i::acce in - let max_w = List.fold_left (fun acc i -> - let (cl,_,_) = Terms.get_from_bag i bag in - max acc (Order.compute_unit_clause_weight cl)) 0 l in - prerr_endline "Statistics :"; - prerr_endline ("Max weight : " ^ (string_of_int max_w)); + let gsteps,esteps = traverse true ([],[]) i in + (List.rev esteps)@gsteps + in + prerr_endline ("steps: " ^ (string_of_int (List.length l))); + let max_w = + List.fold_left + (fun acc i -> + let (cl,_,_) = Terms.get_from_bag i bag in + max acc (Order.compute_unit_clause_weight cl)) 0 l in + prerr_endline "Statistics :"; + prerr_endline ("Max weight : " ^ (string_of_int max_w)); (* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) = Terms.get_from_bag id bag in if d then @@ -423,12 +482,40 @@ module Paramod (B : Orderings.Blob) = struct (Printf.sprintf "Id : %d, selected at %d, weight %d by %s" id it (Order.compute_unit_clause_weight cl) (Pp.pp_proof_step proof))) l;*) - (* prerr_endline "Proof:"; - List.iter (fun x -> - prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l; - *) + List.iter + (fun x -> + let cl,_,_ = Terms.get_from_bag x bag in + prerr_endline (Pp.pp_unit_clause cl)) l; Unsatisfiable [ bag, i, l ] + + let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = + let _initial_timestamp = Unix.gettimeofday () in + let passives = + add_passive_clauses ~no_weight:true passive_empty_set passives + in + let g_passives = + add_passive_goals ~no_weight:true g_passive_empty_set g_passives + in + let g_actives = [] in + let actives = [], IDX.DT.empty in + try + given_clause ~useage ~noinfer:false + bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives + with + | Sup.Success (bag, _, (i,_,_,_)) -> + compute_result bag i + | Stop (Unsatisfiable _) -> Error "stop bug solution found!" + | Stop o -> o + ;; + +let fast_eq_check s goal = + let s = initialize_goal s goal in + try + goal_narrowing 0 2 None s + with + | Sup.Success (bag, _, (i,_,_,_)) -> + compute_result bag i | Stop (Unsatisfiable _) -> Error "stop bug solution found!" | Stop o -> o ;; diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index b195e80c9..b161ae459 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -23,6 +23,8 @@ module type Paramod = | Timeout of int * t Terms.bag type bag = t Terms.bag * int val empty_state : state + val bag_of_state :state -> bag + val replace_bag : state -> bag -> state val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause val forward_infer_step : @@ -30,6 +32,12 @@ module type Paramod = t Terms.unit_clause -> int -> state + val goal_narrowing : + int + -> int + -> float option + -> state + -> state val paramod : useage:bool -> max_steps:int -> @@ -37,6 +45,8 @@ module type Paramod = bag -> g_passives:t Terms.unit_clause list -> passives:t Terms.unit_clause list -> szsontology + val fast_eq_check : + state -> input* input -> szsontology end module Paramod ( B : Orderings.Blob ) : Paramod -- 2.39.2