Added optionnal one pass simplification (instead of keep_simplified)

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 2198ec8bd2be1a3fda3ccf8bd17b770b65655d02..e87a03f52db6e29f1d8152ce23b99a72d921a508 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -23,7 +23,7 @@ module Superposition (B : Terms.Blob) =
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     let debug s =
-      ()(* prerr_endline s *)
+      () (* prerr_endline s *)
     ;;
 
     let rec list_first f = function
@@ -72,6 +72,14 @@ module Superposition (B : Terms.Blob) =
       in
         aux pos ctx t
     ;;
+
+    let vars_of_term t =
+      let rec aux acc = function
+       | Terms.Leaf _ -> acc
+       | Terms.Var i -> if (List.mem i acc) then acc else i::acc
+       | Terms.Node l -> List.fold_left aux acc l
+      in aux [] t
+    ;;
     
     let build_clause bag filter rule t subst vl id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
@@ -85,7 +93,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Utils.add_to_bag bag (0, literal, vl, proof)
+          Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
         in
         Some (bag, uc)
       else
@@ -128,7 +136,7 @@ module Superposition (B : Terms.Blob) =
     (* XXX: possible optimization, if the literal has a "side" already
      * in normal form we should not traverse it again *)
     let demodulate_once bag (id, literal, vl, pr) table =
-      debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));
+      (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       let t = 
         match literal with
         | Terms.Predicate t -> t
@@ -191,20 +199,42 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
+    let one_pass_simplification new_clause (alist,atable) bag =
+      match simplify atable bag new_clause with
+       | None -> None (* new_clause has been discarded *)
+       | Some (bag, clause) ->
+           let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+           let bag, alist, atable = 
+             List.fold_left 
+               (fun (bag, alist, atable as acc) c ->
+                  match simplify ctable bag c with
+                    |None -> acc (* an active clause as been discarded *)
+                    |Some (bag, c1) ->
+                       bag, c :: alist, IDX.index_unit_clause atable c)
+               (bag,[],IDX.DT.empty) alist
+           in
+             Some (clause, bag, (alist,atable))
+    ;;
+
     let simplification_step ~new_cl cl (alist,atable) bag new_clause =
       let atable1 =
        if new_cl then atable else
        IDX.index_unit_clause atable cl
       in
+       (* Simplification of new_clause with :      *
+        * - actives and cl if new_clause is not cl *
+        * - only actives otherwise                 *)
        match simplify atable1 bag new_clause with
-         | None -> (Some cl, None)
+         | None -> (Some cl, None) (* new_clause has been discarded *)
          | Some (bag, clause) ->
+             (* Simplification of each active clause with clause *
+              * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
              let bag, newa, alist, atable = 
                List.fold_left 
                  (fun (bag, newa, alist, atable as acc) c ->
                     match simplify ctable bag c with
-                      |None -> acc
+                      |None -> acc (* an active clause as been discarded *)
                       |Some (bag, c1) ->
                            if (c1 == c) then 
                              bag, newa, c :: alist,
@@ -216,8 +246,10 @@ module Superposition (B : Terms.Blob) =
                if new_cl then
                  (Some cl, Some (clause, (alist,atable), newa, bag))
                else
+                 (* if new_clause is not cl, we simplify cl with clause *)
                  match simplify ctable bag cl with
                    | None ->
+                       (* cl has been discarded *)
                        (None, Some (clause, (alist,atable), newa, bag))
                    | Some (bag,cl1) ->
                        (Some cl1, Some (clause, (alist,atable), newa, bag))