From fedc77dd81516395106ad70468dc1045b5b69263 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Wed, 24 Jun 2009 16:59:41 +0000
Subject: [PATCH] Now inserting hypothesis and goal with zero weight

---
 helm/software/components/ng_paramodulation/paramod.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1c91ee54e..afefb61b6 100644
--- 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
-- 
2.39.2