snaphost: supright almost done

[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..d53b19c8245f8b6513889be718bef52f2c9f9e83 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -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,15 @@ module Utils (B : Terms.Blob) = struct
     fresh_unit_clause maxvar (mk_id (), lit, varlist, proof)
   ;;
 
+  let add_to_bag =
+  let id = ref 0 in
+  fun bag  (_,lit,vl,proof) ->
+    incr id;
+    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