Renamed forward_simplify into simplify and backward_simplify

into simplify_goal

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index a33f1121dd3ceed53364778945541580144cfd8e..1f621ce059b1a3cb1a63a5cdcc114e76ee7df81a 100644 (file)
--- 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 5b88f90cd7a6f47b7a368102a6b5943984a645c4..600e204c850b44531e3d97ac90a699203db70542 100644 (file)
--- 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 cce81944bd497d286b50c22c31d4055c3c4e5228..23477be1a00d3d03b016d42520b69b6d8c7fa145 100644 (file)
--- 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 ->