Fixed conflicts due to problem when merging with UEQ implementation

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

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index c7a0edcca2bff6e43d7d8165278ae0668f7ebcd4..633c32854b284bc79c246515865872dbf01f91e7 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -16,16 +16,22 @@ module Index(B : Orderings.Blob) = struct
 
   module ClauseOT =
     struct 
-      type t = Terms.direction * B.t Terms.clause
+      type t = Terms.direction * (* direction if it is an equality *)
+         bool *                 (* true if indexed literal is positive *)
+         int *                  (* position of literal in clause *)
+         B.t Terms.clause
  
-      let compare (d1,uc1) (d2,uc2) = 
-        let c = Pervasives.compare d1 d2 in
+      let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = 
+        let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
         if c <> 0 then c else U.compare_clause uc1 uc2
       ;;
     end
 
   module ClauseSet : 
-    Set.S with type elt = Terms.direction * B.t Terms.clause
+    Set.S with type elt = Terms.direction * (* direction if it is an equality *)
+                          bool *       (* true if indexed literal is positive *)
+                         int *        (* position of literal in clause *)
+                         B.t Terms.clause
     = Set.Make(ClauseOT)
 
   open Discrimination_tree
@@ -79,18 +85,26 @@ module Index(B : Orderings.Blob) = struct
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
 
-  let index_clause t = function
-    | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
-          DT.index t l (Terms.Left2Right, c)
-    | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
-          DT.index t r (Terms.Right2Left, c)
-    | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->  
-          DT.index  
-           (DT.index t l (Terms.Left2Right, c))
-           r (Terms.Right2Left, c)
-    | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
-    | (_,Terms.Predicate p,_,_) as c ->
-          DT.index t p (Terms.Nodir, c)
+  let index_literal t c is_pos pos = function
+    | Terms.Equation (l,_,_,Terms.Gt) -> 
+          DT.index t l (Terms.Left2Right,is_pos,pos,c)
+    | Terms.Equation (_,r,_,Terms.Lt) ->
+          DT.index t r (Terms.Right2Left,is_pos,pos,c)
+    | Terms.Equation (l,r,_,Terms.Incomparable) ->
+          DT.index
+           (DT.index t l (Terms.Left2Right,is_pos,pos,c))
+           r (Terms.Right2Left,is_pos,pos,c)
+    | Terms.Equation (_,_,_,Terms.Eq) -> assert false
+    | Terms.Predicate p ->
+          DT.index t p (Terms.Nodir,is_pos,pos,c)
+  ;;
+
+  let index_clause t (_,nlit,plit,_,_ as c) =
+    let index_iter is_pos  (t,pos) (lit,sel) =
+      if sel then index_literal t c is_pos pos lit,pos+1 else t,pos+1
+    in
+    let (res,_) = List.fold_left (index_iter false) (t,0) nlit in
+      fst (List.fold_left (index_iter true) (res,0) plit)
   ;;
 
   type active_set = B.t Terms.clause list * DT.t