almost complete superposition right step

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

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 69e451e2e000ef738f8cfd81bb5d24bc5218f951..624b6c99cf3a842fb791a1a552245a61cfcc2c03 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -11,6 +11,15 @@
 
 (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
 
+let rec lexicograph f l1 l2 =
+  match l1, l2 with
+  | [], [] -> 0
+  | x::xs, y::ys ->
+     let c = f x y in
+     if c <> 0 then c else lexicograph f xs ys
+  | [],_ -> ~-1
+  | _,[] -> 1
+;;
 
 module Utils (B : Terms.Blob) = struct
   module Subst = FoSubst.Subst(B) ;;
@@ -25,15 +34,6 @@ module Utils (B : Terms.Blob) = struct
     | _ -> false
   ;;
 
-  let rec lexicograph f l1 l2 =
-    match l1, l2 with
-    | [], [] -> 0
-    | x::xs, y::ys ->
-       let c = f x y in
-       if c <> 0 then c else lexicograph f xs ys
-    | [],_ -> ~-1
-    | _,[] -> 1
-  ;;
 
   let rec compare_foterm x y =
     match x, y with
@@ -118,7 +118,7 @@ module Utils (B : Terms.Blob) = struct
     in
     let lit = 
       match ty with
-      | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.is_eq_predicate eq ->
+      | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
            let o = Order.compare_terms l r in
            Terms.Equation (l, r, ty, o)
       | t -> Terms.Predicate t
@@ -127,4 +127,13 @@ module Utils (B : Terms.Blob) = struct
     fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
   ;;
 
+  let add_to_bag bag  (_,lit,vl,proof) =
+    let id = mk_id () in
+    let clause = (id, lit, vl, proof) in
+    let bag = Terms.M.add id clause bag in
+    bag, clause 
+   ;;
+    
+  let empty_bag = Terms.M.empty ;;
+
 end