From 3a4481e963c6b6e78ad1dce05d75bea992ceaaed Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 12 Jun 2009 11:21:13 +0000 Subject: [PATCH] Renamed forward_simplify into simplify and backward_simplify into simplify_goal --- .../components/ng_paramodulation/paramod.ml | 13 ++++++------- .../components/ng_paramodulation/superposition.ml | 10 +++++----- .../components/ng_paramodulation/superposition.mli | 4 ++-- 3 files changed, 13 insertions(+), 14 deletions(-) diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index a33f1121d..1f621ce05 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -100,25 +100,24 @@ let nparamod metasenv subst context t table = let rec given_clause bag maxvar actives passives g_actives g_passives = (* keep goals demodulated w.r.t. actives and check if solved *) - (* we may move this at the end of infer_right and simplify with - * just new_clauses *) + (* we may move this at the end of infer_right *) let bag, g_actives = List.fold_left (fun (bag,acc) c -> - let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in + let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in bag, c::acc) (bag,[]) g_actives in - (* backward step : superposition left, simplifications on goals *) - debug "Backward infer step..."; + (* superposition left, simplifications on goals *) + debug "infer_left step..."; let bag, maxvar, g_actives, g_passives = match select g_passives with | None -> bag, maxvar, g_actives, g_passives | Some (g_current, g_passives) -> debug ("Selected goal : " ^ Pp.pp_unit_clause g_current); let bag, g_current = - Sup.backward_simplify maxvar (snd actives) bag g_current + Sup.simplify_goal maxvar (snd actives) bag g_current in let bag, maxvar, new_goals = Sup.infer_left bag maxvar g_current actives @@ -152,7 +151,7 @@ let nparamod metasenv subst context t table = | None -> bag, maxvar, actives, passives, g_passives | Some (current, passives) -> debug ("Selected fact : " ^ Pp.pp_unit_clause current); - match Sup.forward_simplify (snd actives) bag current with + match Sup.simplify (snd actives) bag current with | None -> debug ("Discarded fact"); bag, maxvar, actives, passives, g_passives | Some (bag, current) -> diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 5b88f90cd..600e204c8 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -183,7 +183,7 @@ module Superposition (B : Terms.Blob) = ;; (* demodulate and check for subsumption *) - let forward_simplify table bag clause = + let simplify table bag clause = let bag, clause = demodulate bag clause table in if is_identity_clause clause then None else @@ -191,8 +191,8 @@ module Superposition (B : Terms.Blob) = else Some (bag, clause) ;; - (* this is like forward_simplify but raises Success *) - let backward_simplify maxvar table bag clause = + (* this is like simplify but raises Success *) + let simplify_goal maxvar table bag clause = let bag, clause = demodulate bag clause table in if (is_identity_clause clause) || (is_subsumed ~unify:true clause table) then raise (Success (bag, maxvar, clause)) @@ -289,7 +289,7 @@ module Superposition (B : Terms.Blob) = let ctable = IDX.index_unit_clause IDX.DT.empty current in let bag, (alist, atable) = let bag, alist = - HExtlib.filter_map_acc (forward_simplify ctable) bag alist + HExtlib.filter_map_acc (simplify ctable) bag alist in bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist) in @@ -322,7 +322,7 @@ module Superposition (B : Terms.Blob) = debug "Another superposition"; let new_clauses = new_clauses @ additional_new_clauses in let bag, new_clauses = - HExtlib.filter_map_acc (forward_simplify atable) bag new_clauses + HExtlib.filter_map_acc (simplify atable) bag new_clauses in debug "Demodulated new clauses"; bag, maxvar, (alist, atable), new_clauses diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index cce81944b..23477be1a 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -37,14 +37,14 @@ module Superposition (B : Terms.Blob) : B.t Terms.unit_clause -> Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause - val forward_simplify : + val simplify : Index.Index(B).DT.t -> B.t Terms.bag -> B.t Terms.unit_clause -> (B.t Terms.bag * B.t Terms.unit_clause) option (* may raise success *) - val backward_simplify : + val simplify_goal : int -> Index.Index(B).DT.t -> B.t Terms.bag -> -- 2.39.2