X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=86a964c1487f36a7f72deb0c8f2608f621ec2aac;hb=5780119aea0a20e74f7c153add432f5d491ee2a5;hp=a3fd41e21b1d8c5a68a65f88ecc89984c7667ae0;hpb=dce1bca274f93a3bddcc0f6b04cbf126ccff42b0;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index a3fd41e21..86a964c14 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,8 +11,9 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline (Lazy.force s) ;; *)
-let debug _ = ();; 
+let print s = prerr_endline (Lazy.force s) ;; 
+let noprint s = ();;  
+let debug = noprint;;
 
 let monster = 100;;
     
@@ -51,8 +52,15 @@ module type Paramod =
       bag -> 
       g_passives:t Terms.unit_clause list -> 
       passives:t Terms.unit_clause list -> szsontology
+    val demod :
+      state -> input* input -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
+    val nparamod :
+      useage:bool ->
+      max_steps:int ->
+      ?timeout:float ->
+      state -> input* input -> szsontology
   end
 
 module Paramod (B : Orderings.Blob) = struct
@@ -194,6 +202,12 @@ module Paramod (B : Orderings.Blob) = struct
     else WeightPassiveSet.min_elt passives_w
   ;;
 
+  let mk_unit_clause bag maxvar (t,ty) =
+    let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
+    let bag, c = Terms.add_to_bag c bag in
+    (bag, maxvar), c
+  ;;
+
   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
@@ -202,9 +216,11 @@ module Paramod (B : Orderings.Blob) = struct
   ;;
   
   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+
   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
-    let (bag,maxvar), g = mk_goal (bag,maxvar) t in
+    let (bag,maxvar), g = mk_unit_clause bag maxvar t in
     let g_passives = g_passive_empty_set in
     (* if the goal is not an equation we returns an empty
        passive set *)
@@ -248,10 +264,22 @@ module Paramod (B : Orderings.Blob) = struct
       in
         debug (lazy "Performed infer_left step");
 	let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
-        bag, maxvar, actives, passives, g_current::g_actives,
+          bag, maxvar, actives, passives, g_current::g_actives,
     (add_passive_goals g_passives new_goals)
   ;;
 
+  let pp_clauses actives passives =
+    let actives_l, _ = actives in
+    let passive_t,_,_ = passives in
+    let wset = IDX.elems passive_t in
+      ("Actives :" ^ (String.concat ";\n" 
+	(List.map Pp.pp_unit_clause actives_l)))
+      ^ 
+      ("Passives:" ^(String.concat ";\n" 
+        (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
+	       (IDX.ClauseSet.elements wset))))
+  ;;
+
   let forward_infer_step 
       ((bag,maxvar,actives,passives,g_actives,g_passives) as s)  
       current iterno =
@@ -267,17 +295,19 @@ module Paramod (B : Orderings.Blob) = struct
      * P' = P + new'          *)
     debug (lazy "Forward infer step...");
     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
-    let id,_,_,_ = current in
-    let _ = Terms.get_from_bag id bag in 
-
+    noprint (lazy (pp_clauses actives passives));
     match Sup.keep_simplified current actives bag maxvar
     with
       | _,None -> s
       | bag,Some (current,actives) ->
-    debug (lazy "simplified...");
+    debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
+      debug
+	(lazy 
+	 ("New clauses :" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause new_clauses)))); 
       debug (lazy "Demodulating goals with actives...");
       (* keep goals demodulated w.r.t. actives and check if solved *)
       let bag, g_actives = 
@@ -317,44 +347,45 @@ module Paramod (B : Orderings.Blob) = struct
          (passive_set_cardinal passives)))
   ;;
 
- 
+
   (* we just check if any of the active goals is subsumed by a
      passive clause, or if any of the passive goal is subsumed
      by an active or passive clause *) 
   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
     debug (lazy("Last chance " ^ string_of_float
 		  (Unix.gettimeofday())));
-    let active_t = snd actives in
+    let actives_l, active_t = actives in
     let passive_t,wset,_ = passives in
-    let _ = debug
+    let _ = noprint
       (lazy 
-	 ("Passive set :" ^ (String.concat ";\n" 
-	    (List.map (fun _,cl -> Pp.pp_unit_clause cl) 
-	       (WeightPassiveSet.elements wset))))) in
+	 ("Actives :" ^ (String.concat ";\n" 
+	    (List.map Pp.pp_unit_clause actives_l)))) in 
     let wset = IDX.elems passive_t in
-    let _ = debug
+    let _ = noprint
       (lazy 
-	 ("Passive table :" ^(String.concat ";\n" 
-	    (List.map (fun _,cl -> Pp.pp_unit_clause cl)
-	       (IDX.ClauseSet.elements wset))))) in
+	 ("Passives:" ^(String.concat ";\n" 
+	    (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
+	       (IDX.ClauseSet.elements wset))))) in 
     let g_passives = 
       WeightPassiveSet.fold 
 	(fun (_,x) acc ->
 	  if List.exists (Sup.are_alpha_eq x) g_actives then acc
           else x::acc)
 	  (fst g_passives) []
-    in
+    in 
       ignore
       (List.iter
 	(fun x -> 
 	    ignore 
-	      (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
+	     (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
+               Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
        g_passives); 
       ignore
       (List.iter
 	 (fun x -> 
 	    ignore 
-	      (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
+	      (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
+	Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
         (g_actives@g_passives)); 
     raise (Stop (Timeout (maxvar,bag)))
 
@@ -425,6 +456,21 @@ module Paramod (B : Orderings.Blob) = struct
         actives passives g_actives g_passives
   ;;
 
+  let check_and_infer ~no_demod iterno status current =
+    let bag,maxvar,actives,passives,g_actives,g_passives = status in
+    match 
+      Sup.simplify_goal 
+        ~no_demod maxvar (snd actives) bag g_actives current 
+    with
+      | None -> debug (lazy "None"); status
+      | Some (bag,g_current) -> 
+	  let _ = 
+	    debug (lazy("Infer on goal : " 
+			^ Pp.pp_unit_clause g_current)) 
+	  in
+	    backward_infer_step bag maxvar actives passives
+              g_actives g_passives g_current iterno
+
   (* similar to given_clause, but it merely works on goals, 
      in parallel, at each iteration *)
   let rec goal_narrowing iterno max_steps timeout status
@@ -446,19 +492,10 @@ module Paramod (B : Orderings.Blob) = struct
 	   let _ = 
 	     debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) 
 	   in
-           match 
-             Sup.simplify_goal 
-               ~no_demod:false maxvar (snd actives) bag g_actives current 
-           with
-             | None -> acc
-             | Some (bag,g_current) -> 
-		 let _ = 
-		   debug (lazy("Demodulated goal : " 
-			       ^ Pp.pp_unit_clause g_current)) 
-		 in
-		 backward_infer_step bag maxvar actives passives
-                  g_actives g_passives g_current iterno)
-	   status passive_goals
+	     (* we work both on the original goal and the demodulated one*)
+	   let acc = check_and_infer ~no_demod:false iterno acc current
+	   in check_and_infer ~no_demod:true iterno acc current)
+	status passive_goals
     in
       goal_narrowing iterno max_steps timeout newstatus
 
@@ -527,9 +564,19 @@ module Paramod (B : Orderings.Blob) = struct
     | Stop o -> o
   ;;
 
+let demod s goal =
+  let bag,maxvar,actives,passives,g_actives,g_passives = s in
+  let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+  let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+    if g1 = g then GaveUp else compute_result bag i []
+(*
+  if Terms.is_eq_clause g then 
+
+  else GaveUp *)
+
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
-  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  if is_passive_g_set_empty g_passives then Error "not an equation"
   else
   try 
     goal_narrowing 0 2 None s
@@ -540,4 +587,18 @@ let fast_eq_check s goal =
     | Stop o -> o
   ;;
 
+let nparamod ~useage ~max_steps ?timeout s goal =
+  let bag,maxvar,actives,passives,g_actives,g_passives
+      = initialize_goal s goal in
+  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  else
+    try given_clause ~useage ~noinfer:false
+      bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
+  with
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+	compute_result bag i subst
+    | Stop (Unsatisfiable _) -> Error "solution found!"
+    | Stop o -> o
+  ;;
+
 end