Fixed is_identity for facts

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 98bfdde6566deff12d40c57653e3c316935f03c6..1e76758e5b08ead174a79f660761d0954758724c 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -193,7 +193,7 @@ let nparamod rdb metasenv subst context t table =
       given_clause bag maxvar actives passives g_actives g_passives
   in
 
-  let mk_clause ?(no_weight=false) bag maxvar (t,ty) =
+  let mk_clause bag maxvar (t,ty) =
     let (proof,ty) = B.saturate t ty in
     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
     let bag, c = Utils.add_to_bag bag c in
@@ -202,13 +202,14 @@ let nparamod rdb metasenv subst context t table =
   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
   let g_actives = [] in
   let g_passives =
+    (* passive_singleton (Utils.mk_passive_clause goal)*)
     passive_singleton (0,goal)
   in
   let passives, bag, maxvar = 
     List.fold_left
       (fun (cl, bag, maxvar) t -> 
          let bag, maxvar, c = mk_clause bag maxvar t in
-         (add_passive_clause cl c), bag, maxvar)
+         (add_passive_clause ~no_weight:true cl c), bag, maxvar)
       (passive_empty_set, bag, maxvar) table 
   in
   let actives = [], IDX.DT.empty in

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index eaa8f5428bec3a823c9795023b09bc103ec56783..61d6c0589f3ab9952e670ead382f71633ea00ef8 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -178,12 +178,13 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause = function
+    let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof ->
+      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
          (try ignore(Unif.unification vl [] l r); true
          with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Predicate _, _, _ -> assert false       
+      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
@@ -266,7 +267,7 @@ module Superposition (B : Terms.Blob) =
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       let bag, clause = demodulate bag clause table in
-      if is_identity_clause clause then None
+      if is_identity_clause ~unify:false clause then None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
          | None -> Some (bag, clause)
@@ -372,7 +373,7 @@ module Superposition (B : Terms.Blob) =
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
-      if (is_identity_clause clause)
+      if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
       else match is_subsumed ~unify:true bag maxvar clause table with
        | None ->