Implemented handling of Invertible equalities

[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 3491f40196f9a21d8c522d564a49554a1b71be63..520d52396330f9261c0ab58cb1c0bc2af0c4b5c8 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -28,7 +28,8 @@ module type Paramod =
     type bag = t Terms.bag * int
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
-    val paramod : 
+    val paramod :
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
@@ -184,6 +185,7 @@ module Paramod (B : Orderings.Blob) = struct
      * new'= demod A'' new    *
      * P' = P + new'          *)
     debug "Forward infer step...";
+    debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
@@ -199,7 +201,7 @@ module Paramod (B : Orderings.Blob) = struct
                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
           (bag,[]) g_actives 
       in
-      let ctable = IDX.index_unit_clause IDX.DT.empty current in
+      let ctable = IDX.index_unit_clause maxvar IDX.DT.empty current in
       let bag, maxvar, new_goals = 
         List.fold_left 
           (fun (bag,m,acc) g -> 
@@ -208,12 +210,13 @@ module Paramod (B : Orderings.Blob) = struct
           (bag,maxvar,[]) g_actives 
       in
       let bag = Terms.replace_in_bag (current,false,iterno) bag in
+       (* prerr_endline (Pp.pp_bag bag); *)
     bag, maxvar, actives,
     add_passive_clauses passives new_clauses, g_actives,
     add_passive_goals g_passives new_goals
   ;;
  
-  let rec given_clause ~noinfer 
+  let rec given_clause ~useage ~noinfer 
     bag maxvar iterno weight_picks max_steps timeout 
     actives passives g_actives g_passives 
   =
@@ -244,14 +247,14 @@ module Paramod (B : Orderings.Blob) = struct
         else if false then (* activates last chance strategy *)
           begin
            debug("Last chance: "^string_of_float (Unix.gettimeofday()));
-           given_clause ~noinfer:true bag maxvar iterno weight_picks max_steps 
+           given_clause ~useage ~noinfer:true bag maxvar iterno weight_picks max_steps 
              (Some (Unix.gettimeofday () +. 20.))
              actives passives g_actives g_passives;
            raise (Stop (Timeout (maxvar,bag)));
           end
         else raise (Stop (Timeout (maxvar,bag)));
 
-    let use_age = false && (weight_picks = (iterno / 6 + 1)) in
+    let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in
 
@@ -314,7 +317,7 @@ module Paramod (B : Orderings.Blob) = struct
                   if noinfer then
                     let actives = 
                       current::fst actives,
-                      IDX.index_unit_clause (snd actives) current
+                      IDX.index_unit_clause maxvar (snd actives) current
                     in
                     bag,maxvar,actives,passives,g_actives,g_passives
                   else
@@ -341,12 +344,12 @@ module Paramod (B : Orderings.Blob) = struct
       debug
         (Printf.sprintf "Number of passives : %d"
            (passive_set_cardinal passives));
-      given_clause ~noinfer
+      given_clause ~useage ~noinfer
         bag maxvar iterno weight_picks max_steps timeout 
         actives passives g_actives g_passives
   ;;
 
-  let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+  let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
@@ -357,7 +360,7 @@ module Paramod (B : Orderings.Blob) = struct
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
-     given_clause ~noinfer:false
+     given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->