From: denes <??>
Date: Wed, 17 Jun 2009 08:47:34 +0000 (+0000)
Subject: Added optionnal one pass simplification (instead of keep_simplified)
X-Git-Tag: make_still_working~3857
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a15dc157f7e63db12b9a7b59cf00aea108d7e073;p=helm.git

Added optionnal one pass simplification (instead of keep_simplified)
Fix for varlists (we traverse the term to collect occuring variables)
---

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 36adca454..8903ec02f 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,9 +1,9 @@
-let debug s = ()
-(*  prerr_endline s *)
+let debug s =
+  () (* prerr_endline s *)
 ;;
 
 let nparamod rdb metasenv subst context t table =
-  let nb_iter = ref 100 in
+  let nb_iter = ref 200 in
   prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
@@ -39,19 +39,16 @@ let nparamod rdb metasenv subst context t table =
   let rec given_clause bag maxvar actives      
       passives g_actives g_passives =
     
-    decr nb_iter; if !nb_iter = 0 then raise (Failure "Timeout !");
+    decr nb_iter; if !nb_iter = 0 then 
+      (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
+      prerr_endline "Active table :"; 
+       (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
+	  (fst actives));*)
+    raise (Failure "Timeout !");
+
 
-    (* keep goals demodulated w.r.t. actives and check if solved *)
-    (* we may move this at the end of infer_right *) 
-    let bag, g_actives = 
-      List.fold_left 
-        (fun (bag,acc) c -> 
-           let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
-             bag, c::acc) 
-        (bag,[]) g_actives 
-    in
       
-      (* superposition left, simplifications on goals *)
+    (* superposition left, simplifications on goals *)
       debug "infer_left step...";
       let bag, maxvar, g_actives, g_passives =
 	match select g_passives with
@@ -95,16 +92,26 @@ let nparamod rdb metasenv subst context t table =
 	  | Some (current, passives) -> 
 	      debug ("Selected fact : " ^ Pp.pp_unit_clause current);
               match Sup.keep_simplified current actives bag with
+	      (* match Sup.one_pass_simplification current actives bag with *)
 		| None -> aux_simplify passives
-		| Some x -> x
+		| Some x -> x,passives
       in
-      let (current, bag, actives) = aux_simplify passives
+      let (current, bag, actives),passives = aux_simplify passives
       in		    
 	debug ("Fact after simplification :"
 	       ^ Pp.pp_unit_clause current);
 	let bag, maxvar, actives, new_clauses = 
           Sup.infer_right bag maxvar current actives 
 	in
+  debug "Demodulating goals with actives...";
+	  (* keep goals demodulated w.r.t. actives and check if solved *)
+	let bag, g_actives = 
+	  List.fold_left 
+            (fun (bag,acc) c -> 
+               let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
+		 bag, c::acc) 
+            (bag,[]) g_actives 
+	in
 	let ctable = IDX.index_unit_clause IDX.DT.empty current in
 	let bag, maxvar, new_goals = 
 	  List.fold_left 
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 2198ec8bd..e87a03f52 100644
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -23,7 +23,7 @@ module Superposition (B : Terms.Blob) =
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     let debug s =
-      ()(* prerr_endline s *)
+      () (* prerr_endline s *)
     ;;
 
     let rec list_first f = function
@@ -72,6 +72,14 @@ module Superposition (B : Terms.Blob) =
       in
         aux pos ctx t
     ;;
+
+    let vars_of_term t =
+      let rec aux acc = function
+	| Terms.Leaf _ -> acc
+	| Terms.Var i -> if (List.mem i acc) then acc else i::acc
+	| Terms.Node l -> List.fold_left aux acc l
+      in aux [] t
+    ;;
     
     let build_clause bag filter rule t subst vl id id2 pos dir =
       let proof = Terms.Step(rule,id,id2,dir,pos,subst) in
@@ -85,7 +93,7 @@ module Superposition (B : Terms.Blob) =
           | t -> Terms.Predicate t
         in
         let bag, uc = 
-          Utils.add_to_bag bag (0, literal, vl, proof)
+          Utils.add_to_bag bag (0, literal, vars_of_term t, proof)
         in
         Some (bag, uc)
       else
@@ -128,7 +136,7 @@ module Superposition (B : Terms.Blob) =
     (* XXX: possible optimization, if the literal has a "side" already
      * in normal form we should not traverse it again *)
     let demodulate_once bag (id, literal, vl, pr) table =
-      debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));
+      (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       let t = 
         match literal with
         | Terms.Predicate t -> t
@@ -191,20 +199,42 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
+    let one_pass_simplification new_clause (alist,atable) bag =
+      match simplify atable bag new_clause with
+	| None -> None (* new_clause has been discarded *)
+	| Some (bag, clause) ->
+	    let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+	    let bag, alist, atable = 
+	      List.fold_left 
+		(fun (bag, alist, atable as acc) c ->
+		   match simplify ctable bag c with
+		     |None -> acc (* an active clause as been discarded *)
+		     |Some (bag, c1) ->
+			bag, c :: alist, IDX.index_unit_clause atable c)
+		(bag,[],IDX.DT.empty) alist
+	    in
+	      Some (clause, bag, (alist,atable))
+    ;;
+
     let simplification_step ~new_cl cl (alist,atable) bag new_clause =
       let atable1 =
 	if new_cl then atable else
 	IDX.index_unit_clause atable cl
       in
+	(* Simplification of new_clause with :      *
+	 * - actives and cl if new_clause is not cl *
+	 * - only actives otherwise                 *)
 	match simplify atable1 bag new_clause with
-	  | None -> (Some cl, None)
+	  | None -> (Some cl, None) (* new_clause has been discarded *)
 	  | Some (bag, clause) ->
+	      (* Simplification of each active clause with clause *
+	       * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
 	      let bag, newa, alist, atable = 
 		List.fold_left 
 		  (fun (bag, newa, alist, atable as acc) c ->
 		     match simplify ctable bag c with
-		       |None -> acc
+		       |None -> acc (* an active clause as been discarded *)
 		       |Some (bag, c1) ->
 			    if (c1 == c) then 
 			      bag, newa, c :: alist,
@@ -216,8 +246,10 @@ module Superposition (B : Terms.Blob) =
 		if new_cl then
 		  (Some cl, Some (clause, (alist,atable), newa, bag))
 		else
+		  (* if new_clause is not cl, we simplify cl with clause *)
 		  match simplify ctable bag cl with
 		    | None ->
+			(* cl has been discarded *)
 			(None, Some (clause, (alist,atable), newa, bag))
 		    | Some (bag,cl1) ->
 			(Some cl1, Some (clause, (alist,atable), newa, bag))
diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index d7efb1b42..6deb0a4eb 100644
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -51,6 +51,13 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
             B.t Terms.bag * B.t Terms.unit_clause
 
+    val one_pass_simplification:
+      B.t Terms.unit_clause ->
+      Index.Index(B).active_set ->
+      B.t Terms.bag ->
+      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+
+
     val keep_simplified:
       B.t Terms.unit_clause ->
       Index.Index(B).active_set ->