X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=7fc13b504290aebbf11bbcfbf5032131ce60ad7d;hb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;hp=de32ab5ddf8b7e0fe1b8984ed4bdad4e4d4c3970;hpb=f59b591eb48a06518b34d7f809bee51989307404;p=helm.git diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index de32ab5dd..7fc13b504 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -202,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 @@ -210,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 *) @@ -268,7 +276,7 @@ module Paramod (B : Orderings.Blob) = struct (List.map Pp.pp_unit_clause actives_l))) ^ ("Passives:" ^(String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (List.map (fun (_,cl) -> Pp.pp_unit_clause cl) (IDX.ClauseSet.elements wset)))) ;; @@ -287,7 +295,7 @@ 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))))); - debug (lazy (pp_clauses actives passives)); + noprint (lazy (pp_clauses actives passives)); match Sup.keep_simplified current actives bag maxvar with | _,None -> s @@ -356,7 +364,7 @@ module Paramod (B : Orderings.Blob) = struct let _ = noprint (lazy ("Passives:" ^(String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (List.map (fun (_,cl) -> Pp.pp_unit_clause cl) (IDX.ClauseSet.elements wset))))) in let g_passives = WeightPassiveSet.fold @@ -566,7 +574,7 @@ let demod s goal = 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