From 550489243bb7bbd995ce3484cbb3a3711371b949 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 11 Jan 2010 11:27:54 +0000 Subject: [PATCH] 1. New paramodulation function 2. goal narrowing works both on the current goal both before and after demodulation --- .../components/ng_paramodulation/paramod.ml | 68 +++++++++++++------ .../components/ng_paramodulation/paramod.mli | 7 ++ 2 files changed, 55 insertions(+), 20 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index a3fd41e21..7c934df1e 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;; @@ -53,6 +53,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 @@ -248,7 +253,7 @@ 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) ;; @@ -278,6 +283,10 @@ module Paramod (B : Orderings.Blob) = struct 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 = @@ -324,17 +333,16 @@ module Paramod (B : Orderings.Blob) = struct 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 actives_l, active_t = actives in let passive_t,wset,_ = passives in let _ = debug (lazy - ("Passive set :" ^ (String.concat ";\n" - (List.map (fun _,cl -> Pp.pp_unit_clause cl) - (WeightPassiveSet.elements wset))))) in + ("Actives :" ^ (String.concat ";\n" + (List.map Pp.pp_unit_clause actives_l)))) in let wset = IDX.elems passive_t in let _ = debug (lazy - ("Passive table :" ^(String.concat ";\n" + ("Passives:" ^(String.concat ";\n" (List.map (fun _,cl -> Pp.pp_unit_clause cl) (IDX.ClauseSet.elements wset))))) in let g_passives = @@ -425,6 +433,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:false maxvar (snd actives) bag g_actives current + with + | 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 @@ -446,19 +469,10 @@ 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 + (* 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) + status passive_goals in goal_narrowing iterno max_steps timeout newstatus @@ -540,4 +554,18 @@ let fast_eq_check s goal = | 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 + ;; + end diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 321d0f897..1142b03c7 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -48,6 +48,13 @@ 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 ) : Paramod -- 2.39.2