X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Findex.ml;h=6c26e7b86ab82cfeab8996b743d076bd614560f3;hb=637114791874df9ebc4e0f0936513c71886a913f;hp=ca30c9b504ef126f72620205c5f2b586e949783c;hpb=f3c6deea5fa1ed58847d7fcdf597193e2c5c7ddb;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index ca30c9b50..6c26e7b86 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -79,4 +79,18 @@ module Index(B : Terms.Blob) = struct
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
 
+  let index_unit_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)
+  ;;
+
 end