X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hb=5780119aea0a20e74f7c153add432f5d491ee2a5;hp=7c934df1e59cd48373a65d5a66ff11d98237eb82;hpb=550489243bb7bbd995ce3484cbb3a3711371b949;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 7c934df1e..86a964c14 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;; @@ -51,6 +52,8 @@ module type Paramod = bag -> g_passives:t Terms.unit_clause list -> passives:t Terms.unit_clause list -> szsontology + val demod : + state -> input* input -> szsontology val fast_eq_check : state -> input* input -> szsontology val nparamod : @@ -199,6 +202,12 @@ module Paramod (B : Orderings.Blob) = struct else WeightPassiveSet.min_elt passives_w ;; + let mk_unit_clause bag maxvar (t,ty) = + let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in + let bag, c = Terms.add_to_bag c bag in + (bag, maxvar), c + ;; + let mk_clause bag maxvar (t,ty) = let (proof,ty) = B.saturate t ty in let c, maxvar = Utils.mk_unit_clause maxvar ty proof in @@ -207,9 +216,11 @@ 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 (bag,maxvar), g = mk_unit_clause bag maxvar t in let g_passives = g_passive_empty_set in (* if the goal is not an equation we returns an empty passive set *) @@ -257,6 +268,18 @@ module Paramod (B : Orderings.Blob) = struct (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 = @@ -272,14 +295,12 @@ 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 - + noprint (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 @@ -326,7 +347,7 @@ 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 *) @@ -335,34 +356,36 @@ module Paramod (B : Orderings.Blob) = struct (Unix.gettimeofday()))); let actives_l, active_t = actives in let passive_t,wset,_ = passives in - let _ = debug + let _ = noprint (lazy ("Actives :" ^ (String.concat ";\n" (List.map Pp.pp_unit_clause actives_l)))) in let wset = IDX.elems passive_t in - let _ = debug + let _ = noprint (lazy ("Passives:" ^(String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) - (IDX.ClauseSet.elements wset))))) in + (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))) @@ -437,9 +460,9 @@ module Paramod (B : Orderings.Blob) = struct let bag,maxvar,actives,passives,g_actives,g_passives = status in match Sup.simplify_goal - ~no_demod:false maxvar (snd actives) bag g_actives current + ~no_demod maxvar (snd actives) bag g_actives current with - | None -> status + | None -> debug (lazy "None"); status | Some (bag,g_current) -> let _ = debug (lazy("Infer on goal : " @@ -469,9 +492,9 @@ module Paramod (B : Orderings.Blob) = struct let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in - (* awe work both on the original goal and the demodulated one*) - let acc = check_and_infer ~no_demod:true iterno acc current - in check_and_infer ~no_demod:false iterno acc current) + (* 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 @@ -541,9 +564,19 @@ module Paramod (B : Orderings.Blob) = struct | Stop o -> o ;; +let demod s goal = + let bag,maxvar,actives,passives,g_actives,g_passives = s in + let (bag,maxvar), g = mk_goal (bag,maxvar) goal in + let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in + if g1 = g then GaveUp else compute_result bag i [] +(* + if Terms.is_eq_clause g then + + else GaveUp *) + let fast_eq_check s goal = let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in - if is_passive_g_set_empty g_passives then Error "not an equation" + if is_passive_g_set_empty g_passives then Error "not an equation" else try goal_narrowing 0 2 None s