Fixed nasty bug in superposition and freshing of clauses

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

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1f64314c9df48197d718debd7b937b0de1d3cc6c..8bbf6e1606162c47eca6f15a8490e1ba2f7fa3f3 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -64,16 +64,18 @@ module Paramod (B : Orderings.Blob) = struct
   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
   module AgePassiveSet = Set.Make(AgeOrderedPassives)
 
-  let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
-    let cl = if no_weight then (0,cl)
-    else Clauses.mk_passive_clause cl in
-    WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
+  let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
+    let (w,cl) = Clauses.mk_passive_clause cl in
+    (* let cl = (w+bonus_weight,cl) in *)
+    let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in
+   WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   ;;
 
-  let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
-    let g = if no_weight then (0,g)
-    else Clauses.mk_passive_goal g in
-    WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+  let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
+    let (w,g) = Clauses.mk_passive_goal g in
+    (* let g = (w+bonus_weight,g) in *)
+    let g = if bonus_weight = 0 then (w,g) else (0,g) in
+   WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
   ;;
 
   let remove_passive_clause (passives_w,passives_a) cl =
@@ -82,20 +84,20 @@ module Paramod (B : Orderings.Blob) = struct
       passives_w,passives_a
   ;;
 
-  let add_passive_clauses ?(no_weight=false)
+  let add_passive_clauses ?(bonus_weight=0)
       (passives_w,passives_a) new_clauses =
     let new_clauses_w,new_clauses_a =
-      List.fold_left (add_passive_clause ~no_weight)
+      List.fold_left (add_passive_clause ~bonus_weight)
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
        AgePassiveSet.union new_clauses_a passives_a)
   ;;
 
-  let add_passive_goals ?(no_weight=false)
+  let add_passive_goals ?(bonus_weight=0)
       (passives_w,passives_a) new_clauses =
     let new_clauses_w,new_clauses_a =
-      List.fold_left (add_passive_goal ~no_weight)
+      List.fold_left (add_passive_goal ~bonus_weight)
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
@@ -342,14 +344,14 @@ module Paramod (B : Orderings.Blob) = struct
       let bag,c = Terms.add_to_bag c bag in
       (bag,maxvar,c::l)
     in
-    let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
     let bag,maxvar,goals = build_clause (bag,maxvar,[]) goal in
+    let bag,maxvar,hypotheses = List.fold_left build_clause (bag,maxvar,[]) hypotheses in
     let goal = match goals with | [g] -> g | _ -> assert false in
     let passives =
-      add_passive_clauses ~no_weight:true passive_empty_set hypotheses
+      add_passive_clauses ~bonus_weight:(-1000) passive_empty_set hypotheses
     in
     let g_passives =
-      add_passive_goal ~no_weight:true passive_empty_set goal
+      add_passive_goal ~bonus_weight:(-1000) passive_empty_set goal
     in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in