From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 11 Jan 2010 11:27:54 +0000 (+0000)
Subject: 1. New paramodulation function
X-Git-Tag: make_still_working~3128
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=550489243bb7bbd995ce3484cbb3a3711371b949;p=helm.git

1. New paramodulation function
2. goal narrowing works both on the current goal both before and after
demodulation
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index a3fd41e21..7c934df1e 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 (* let debug s = prerr_endline (Lazy.force s) ;; *)
-let debug _ = ();; 
+let debug _ = ();;  
 
 let monster = 100;;
     
@@ -53,6 +53,11 @@ module type Paramod =
       passives:t Terms.unit_clause list -> 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
@@ -248,7 +253,7 @@ 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)
   ;;
 
@@ -278,6 +283,10 @@ module Paramod (B : Orderings.Blob) = struct
     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 = 
@@ -324,17 +333,16 @@ module Paramod (B : Orderings.Blob) = struct
   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
       (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
       (lazy 
-	 ("Passive table :" ^(String.concat ";\n" 
+	 ("Passives:" ^(String.concat ";\n" 
 	    (List.map (fun _,cl -> Pp.pp_unit_clause cl)
 	       (IDX.ClauseSet.elements wset))))) in
     let g_passives = 
@@ -425,6 +433,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:false maxvar (snd actives) bag g_actives current 
+    with
+      | 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 +469,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
+	     (* awe work both on the original goal and the demodulated one*)
+	   let acc = check_and_infer ~no_demod:true iterno acc current
+	   in check_and_infer ~no_demod:false iterno acc current)
+	status passive_goals
     in
       goal_narrowing iterno max_steps timeout newstatus
 
@@ -540,4 +554,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
diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 321d0f897..1142b03c7 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -48,6 +48,13 @@ module type Paramod =
       passives:t Terms.unit_clause list -> 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 ) : Paramod