Now inserting hypothesis and goal with zero weight

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1c91ee54ecdc8141b7fe2c0a037572b565b7d3e9..afefb61b6324a2b17c88c827975e7bfe704b0387 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -35,8 +35,9 @@ let nparamod rdb metasenv subst context t table =
   in
   let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
   let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
-  let add_passive_clause (passives_w,passives_a) cl =
-    let cl = Utils.mk_passive_clause cl in
+  let add_passive_clause ?(no_weight=true) (passives_w,passives_a) cl =
+    let cl = if no_weight then (0,cl)
+    else Utils.mk_passive_clause cl in
     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   in
   let remove_passive_clause (passives_w,passives_a) cl =
@@ -192,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 bag maxvar (t,ty) =
+  let mk_clause ?(no_weight=false) 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
@@ -201,7 +202,7 @@ 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