X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=8abdaaec509301e7ef7cae20300601925d9739f0;hb=37b52567b8aa1bf5807767d94b96594c0e640588;hp=3af1a38e448c459369a0bead452a7b4c84cc6363;hpb=646da3fc52fa905a67959cfa1191eb5c96edaef1;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 3af1a38e4..8abdaaec5 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,8 +11,9 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -let debug s = prerr_endline (Lazy.force s) ;; -(* let debug _ = ();; *) +let print s = prerr_endline (Lazy.force s) ;; +let noprint s = ();; +let debug = noprint;; let monster = 100;; @@ -21,7 +22,8 @@ module type Paramod = type t type input type szsontology = - | Unsatisfiable of (t Terms.bag * int * int list) list + | Unsatisfiable of + (t Terms.bag * int * t Terms.substitution * int list) list | GaveUp | Error of string | Timeout of int * t Terms.bag @@ -52,6 +54,11 @@ module type Paramod = passives:t Terms.unit_clause list -> szsontology val fast_eq_check : state -> input* input -> szsontology + val nparamod : + useage:bool -> + max_steps:int -> + ?timeout:float -> + state -> input* input -> szsontology end module Paramod (B : Orderings.Blob) = struct @@ -80,7 +87,8 @@ module Paramod (B : Orderings.Blob) = struct type input = B.input type bag = B.t Terms.bag * int type szsontology = - | Unsatisfiable of (B.t Terms.bag * int * int list) list + | Unsatisfiable of + (B.t Terms.bag * int * B.t Terms.substitution * int list) list | GaveUp | Error of string | Timeout of int * B.t Terms.bag @@ -204,7 +212,12 @@ module Paramod (B : Orderings.Blob) = struct 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 + (* if the goal is not an equation we returns an empty + passive set *) + let g_passives = + if Terms.is_eq_clause g then add_passive_goal g_passives g + else g_passives + in (bag,maxvar,actives,passives,[],g_passives) @@ -241,10 +254,22 @@ module Paramod (B : Orderings.Blob) = struct in debug (lazy "Performed infer_left step"); let bag = Terms.replace_in_bag (g_current,false,iterno) bag in - bag, maxvar, actives, passives, g_current::g_actives, + bag, maxvar, actives, passives, g_current::g_actives, (add_passive_goals g_passives new_goals) ;; + let pp_clauses actives passives = + let actives_l, _ = actives in + let passive_t,_,_ = passives in + let wset = IDX.elems passive_t in + ("Actives :" ^ (String.concat ";\n" + (List.map Pp.pp_unit_clause actives_l))) + ^ + ("Passives:" ^(String.concat ";\n" + (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (IDX.ClauseSet.elements wset)))) + ;; + let forward_infer_step ((bag,maxvar,actives,passives,g_actives,g_passives) as s) current iterno = @@ -260,17 +285,19 @@ 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 - + debug (lazy (pp_clauses actives passives)); match Sup.keep_simplified current actives bag maxvar with | _,None -> s | bag,Some (current,actives) -> - debug (lazy "simplified..."); + debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current))); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in + debug + (lazy + ("New clauses :" ^ (String.concat ";\n" + (List.map Pp.pp_unit_clause new_clauses)))); debug (lazy "Demodulating goals with actives..."); (* keep goals demodulated w.r.t. actives and check if solved *) let bag, g_actives = @@ -310,33 +337,45 @@ module Paramod (B : Orderings.Blob) = struct (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 actives_l, active_t = actives in + let passive_t,wset,_ = passives in + let _ = noprint + (lazy + ("Actives :" ^ (String.concat ";\n" + (List.map Pp.pp_unit_clause actives_l)))) in + let wset = IDX.elems passive_t in + let _ = noprint + (lazy + ("Passives:" ^(String.concat ";\n" + (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (IDX.ClauseSet.elements wset))))) 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 + in ignore (List.iter (fun x -> ignore - (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x)) + (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x)); + 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)) + (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x)); + Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x)) (g_actives@g_passives)); raise (Stop (Timeout (maxvar,bag))) @@ -407,6 +446,21 @@ module Paramod (B : Orderings.Blob) = struct actives passives g_actives g_passives ;; + let check_and_infer ~no_demod iterno status current = + let bag,maxvar,actives,passives,g_actives,g_passives = status in + match + Sup.simplify_goal + ~no_demod maxvar (snd actives) bag g_actives current + with + | None -> debug (lazy "None"); status + | Some (bag,g_current) -> + let _ = + debug (lazy("Infer on goal : " + ^ Pp.pp_unit_clause g_current)) + in + backward_infer_step bag maxvar actives passives + g_actives g_passives g_current iterno + (* similar to given_clause, but it merely works on goals, in parallel, at each iteration *) let rec goal_narrowing iterno max_steps timeout status @@ -428,23 +482,14 @@ module Paramod (B : Orderings.Blob) = struct 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 + (* we work both on the original goal and the demodulated one*) + let acc = check_and_infer ~no_demod:false iterno acc current + in check_and_infer ~no_demod:true iterno acc current) + status passive_goals in goal_narrowing iterno max_steps timeout newstatus - let compute_result bag i = + let compute_result bag i subst = let l = let rec traverse ongoal (accg,acce) i = match Terms.get_from_bag i bag with @@ -462,14 +507,13 @@ module Paramod (B : Orderings.Blob) = struct let gsteps,esteps = traverse true ([],[]) i in (List.rev esteps)@gsteps in - prerr_endline ("steps: " ^ (string_of_int (List.length l))); + debug (lazy ("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)); + debug (lazy ("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 @@ -482,12 +526,13 @@ 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 -> - let cl,_,_ = Terms.get_from_bag x bag in - prerr_endline (Pp.pp_unit_clause cl)) l; - Unsatisfiable [ bag, i, l ] + debug (lazy ("Proof:" ^ + (String.concat "\n" + (List.map + (fun x -> + let cl,_,_ = Terms.get_from_bag x bag in + Pp.pp_unit_clause cl) l)))); + Unsatisfiable [ bag, i, subst, l ] let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives = let _initial_timestamp = Unix.gettimeofday () in @@ -503,20 +548,36 @@ module Paramod (B : Orderings.Blob) = struct 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!" + | Sup.Success (bag, _, (i,_,_,_),subst) -> + compute_result bag i subst + | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;; let fast_eq_check s goal = - let s = initialize_goal s goal in + let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in + if is_passive_g_set_empty g_passives then Error "not an equation" + else try goal_narrowing 0 2 None s with - | Sup.Success (bag, _, (i,_,_,_)) -> - compute_result bag i - | Stop (Unsatisfiable _) -> Error "stop bug solution found!" + | Sup.Success (bag, _, (i,_,_,_),subst) -> + compute_result bag i subst + | Stop (Unsatisfiable _) -> Error "solution found!" + | Stop o -> o + ;; + +let nparamod ~useage ~max_steps ?timeout s goal = + let bag,maxvar,actives,passives,g_actives,g_passives + = initialize_goal s goal in + if is_passive_g_set_empty g_passives then Error "not an equation" + else + try given_clause ~useage ~noinfer:false + bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives + with + | Sup.Success (bag, _, (i,_,_,_),subst) -> + compute_result bag i subst + | Stop (Unsatisfiable _) -> Error "solution found!" | Stop o -> o ;;