Implemented keep_simplified.

If a candidate for forward inference is discarded, another is selected

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 1f621ce059b1a3cb1a63a5cdcc114e76ee7df81a..b301e800547aa40aa0e2c61a98af0916f2a8ccca 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,70 +1,9 @@
-(*let nparamod metasenv subst context t table =
-  prerr_endline "========================================";
-  let module C = struct
-    let metasenv = metasenv
-    let subst = subst
-    let context = context
-  end
-  in
-  let module B = NCicBlob.NCicBlob(C) in
-  let module Pp = Pp.Pp (B) in
-  let module FU = FoUnif.Founif(B) in
-  let module IDX = Index.Index(B) in
-  let module Sup = Superposition.Superposition(B) in
-  let module Utils = FoUtils.Utils(B) in*)
-(*
-  let test_unification _ = function
-    | Terms.Node [_; _; lhs; rhs] ->
-       prerr_endline "Unification test :";
-       prerr_endline (Pp.pp_foterm lhs);
-       prerr_endline (Pp.pp_foterm rhs);
-        FU.unification [] [] lhs rhs
-    | _ -> assert false
-  in
-  let subst,vars = test_unification [] res in
-    prerr_endline "Result :";
-    prerr_endline (Pp.pp_foterm res);
-    prerr_endline "Substitution :";
-    prerr_endline (Pp.pp_substitution subst)
-*)
-(*
-
-  let mk_clause maxvar t =
-    let ty = B.embed t in
-    let proof = B.embed (NCic.Rel ~-1) in
-    Utils.mk_unit_clause maxvar ty proof 
-  in
-  let clause, maxvar = mk_clause 0 t in
-  prerr_endline "Input clause :";
-  prerr_endline (Pp.pp_unit_clause clause);
-  let bag = Utils.empty_bag in
-  let active_clauses, maxvar = 
-    List.fold_left
-      (fun (cl,maxvar) t -> 
-         let c, m = mk_clause maxvar t in
-         c::cl, m)
-      ([],maxvar) table 
-  in
-  let table =  
-    List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
-  in
-  prerr_endline "Active table:";
-  List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
-  let bag, maxvar, _, newclauses = 
-    Sup.infer_right bag maxvar clause (active_clauses, table)
-  in
-  prerr_endline "Output clauses :";
-  List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
-  (* prerr_endline "Proofs: ";
-  prerr_endline (Pp.pp_bag bag); *)
-  prerr_endline "========================================";
-;;
-*)
-let debug s =
-  prerr_endline s
+let debug s = ()
+(*  prerr_endline s *)
 ;;
 
 let nparamod metasenv subst context t table =
+  let nb_iter = ref 100 in
   prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
@@ -97,8 +36,11 @@ let nparamod metasenv subst context t table =
     else let cl = PassiveSet.min_elt passives in
       Some (snd cl,PassiveSet.remove cl passives)
   in
-  let rec given_clause bag maxvar actives passives g_actives g_passives =
+  let rec given_clause bag maxvar actives      
+      passives g_actives g_passives =
     
+    decr nb_iter; if !nb_iter = 0 then 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 = 
@@ -147,34 +89,38 @@ let nparamod metasenv subst context t table =
        * P' = P + new'          *)
       debug "Forward infer step...";
     let bag, maxvar, actives, passives, g_passives =
-      match select passives with
-      | None -> bag, maxvar, actives, passives, g_passives
-      | Some (current, passives) -> 
-         debug ("Selected fact : " ^ Pp.pp_unit_clause current);
-          match Sup.simplify (snd actives) bag current with
-          | None -> debug ("Discarded fact");
-             bag, maxvar, actives, passives, g_passives
-          | Some (bag, current) ->
-             debug ("Fact after simplification :" ^ Pp.pp_unit_clause current);
-              let bag, maxvar, actives, new_clauses = 
-                Sup.infer_right bag maxvar current actives 
-              in
-             let ctable = IDX.index_unit_clause IDX.DT.empty current in
-             let bag, maxvar, new_goals = 
-               List.fold_left 
-                 (fun (bag,m,acc) g -> 
-                    let bag, m, ng = Sup.infer_left bag maxvar g
-                      ([current],ctable) in
-                      bag,m,ng@acc) 
-                 (bag,maxvar,[]) g_actives 
-             in
-             let new_clauses = List.fold_left add_passive_clause
-               PassiveSet.empty new_clauses in
-             let new_goals = List.fold_left add_passive_clause
-               PassiveSet.empty new_goals in
-               bag, maxvar, actives,
-             PassiveSet.union new_clauses passives,
-             PassiveSet.union new_goals g_passives
+      let rec aux_simplify passives =
+       match select passives with
+         | None -> assert false
+         | Some (current, passives) -> 
+             debug ("Selected fact : " ^ Pp.pp_unit_clause current);
+              match Sup.keep_simplified current actives bag with
+               | None -> aux_simplify passives
+               | Some x -> x
+      in
+      let (current, bag, actives) = 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
+       let ctable = IDX.index_unit_clause IDX.DT.empty current in
+       let bag, maxvar, new_goals = 
+         List.fold_left 
+           (fun (bag,m,acc) g -> 
+              let bag, m, ng = Sup.infer_left bag maxvar g
+                ([current],ctable) in
+                bag,m,ng@acc) 
+           (bag,maxvar,[]) g_actives 
+       in
+       let new_clauses = List.fold_left add_passive_clause
+         PassiveSet.empty new_clauses in
+       let new_goals = List.fold_left add_passive_clause
+         PassiveSet.empty new_goals in
+         bag, maxvar, actives,
+      PassiveSet.union new_clauses passives,
+      PassiveSet.union new_goals g_passives
     in
       prerr_endline
        (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
@@ -204,6 +150,7 @@ let nparamod metasenv subst context t table =
   try given_clause bag maxvar actives passives g_actives g_passives
   with Sup.Success (bag, _, mp) ->
     prerr_endline "YES!";
-    prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp);
+    prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp)
     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
+    | Failure _ -> prerr_endline "FAILURE"
 ;;

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 4142a35b67205f1cc19638931420260b74a2fd7f..046799a775149470bd7162252b023e582ffb9e99 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -191,27 +191,67 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
-    let rec keep_simplified (alist,atable) bag newc = 
-      match newc with
-       | [] -> bag, (alist,atable)
-       | hd::tl -> 
-           (match simplify atable bag hd with
-              | None -> keep_simplified (alist,atable) bag tl
-              | Some (bag, 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) c ->
-                       let bag, c1 = demodulate bag c ctable in
-                       if (c1 == c) then 
-                          bag, newa, c :: alist, IDX.index_unit_clause atable c
-                       else
-                         bag, c :: newa, alist, atable)
-                    (bag,[],[],IDX.DT.empty) alist
-                  in
-                    keep_simplified (alist, atable) bag newa)
+    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
+       match simplify atable1 bag new_clause with
+         | None -> (Some cl, None)
+         | Some (bag, 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
+                      |Some (bag, c1) ->
+                           if (c1 == c) then 
+                             bag, newa, c :: alist,
+                           IDX.index_unit_clause atable c
+                           else
+                             bag, c1 :: newa, alist, atable)             
+                 (bag,[],[],IDX.DT.empty) alist
+             in
+               if new_cl then
+                 (Some cl, Some (clause, (alist,atable), newa, bag))
+               else
+                 match simplify ctable bag cl with
+                   | None ->
+                       (None, Some (clause, (alist,atable), newa, bag))
+                   | Some (bag,cl1) ->
+                       (Some cl1, Some (clause, (alist,atable), newa, bag))
     ;;
 
+    let keep_simplified cl (alist,atable) bag =
+      let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
+       if new_cl then
+         match simplification_step ~new_cl cl (alist,atable) bag cl with
+           | (None, _) -> assert false
+           | (Some _, None) -> None
+           | (Some _, Some (clause, (alist,atable), newa, bag)) ->
+               keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
+                 bag (newa@newc)
+       else
+         match newc with
+           | [] -> Some (cl, bag, (alist,atable))
+           | hd::tl ->
+               match simplification_step ~new_cl cl
+                 (alist,atable) bag hd with
+                 | (None,None) -> assert false
+                 | (Some _,None) ->
+                     keep_simplified_aux ~new_cl cl (alist,atable) bag tl
+                 | (None, Some _) -> None
+                 | (Some cl1, Some (clause, (alist,atable), newa, bag)) ->
+                     let alist,atable =
+                       (clause::alist, IDX.index_unit_clause atable clause)
+                     in
+                       keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
+                         bag (newa@tl)
+      in
+       keep_simplified_aux ~new_cl:true cl (alist,atable) bag []
+    ;;                 
+         
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag clause = 
       let bag, clause = demodulate bag clause table in
@@ -306,14 +346,16 @@ module Superposition (B : Terms.Blob) =
     (* the current equation is normal w.r.t. demodulation with atable
      * (and is not the identity) *)
     let infer_right bag maxvar current (alist,atable) = 
-      (* We demodulate actives clause with current *)
+      (* We demodulate actives clause with current until all *
+       * active clauses are reduced w.r.t each other         *)
+      (* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
-      let bag, (alist, atable) = 
+      (* let bag, (alist, atable) = 
         let bag, alist = 
           HExtlib.filter_map_acc (simplify ctable) bag alist
         in
         bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
-      in
+      in*)
        debug "Simplified active clauses with fact";
       (* We superpose active clauses with current *)
       let bag, maxvar, new_clauses =

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index 23477be1a00d3d03b016d42520b69b6d8c7fa145..d7efb1b42b8921d4bb225575cc5bab1aea7639a9 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -51,7 +51,11 @@ module Superposition (B : Terms.Blob) :
           B.t Terms.unit_clause ->
             B.t Terms.bag * B.t Terms.unit_clause
 
-  end
-
+    val keep_simplified:
+      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
 
 
+  end