proof reconstruction almost OK

[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 36adca45413def9a1fa5214571a84c92edcbfbca..f0cd03758594d92411284fd0e1945d86d21a3967 100644 (file)
--- 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 
@@ -158,27 +165,42 @@ let nparamod rdb metasenv subst context t table =
           Set.Make(struct type t=int let compare=Pervasives.compare end)
         in
         let all id = 
-          let rec traverse acc i =
+          let rec traverse ongoal (accg,acce) i =
             match Terms.M.find i bag with
-            | (_,_,_,Terms.Exact _) -> acc
+            | (_,_,_,Terms.Exact _) -> accg, acce
             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) -> 
-               traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2    
+               let accg, acce = 
+                 if ongoal then C.add i1 accg, acce
+                 else accg, C.add i1 acce
+               in
+               let acce = C.add i2 acce in
+                 traverse false (traverse ongoal (accg,acce) i1) i2    
           in
-           C.elements (traverse C.empty id)
+            traverse true (C.empty,C.empty) id
+        in
+        let esteps = 
+          S.topological_sort (C.elements (snd (all i))) 
+           (fun i -> C.elements (snd (all i)))
+        in
+        let gsteps = 
+          S.topological_sort (C.elements (fst (all i))) 
+           (fun i -> C.elements (fst (all i)))
         in
-        S.topological_sort (all i) all
+        let gsteps = List.rev gsteps in
+        esteps@gsteps
       in
       prerr_endline "YES!";
       prerr_endline "Proof:"; 
       List.iter (fun x -> 
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
-      let proofterm = B.mk_proof bag l in
+      let proofterm = B.mk_proof bag i l in
       prerr_endline
        (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
          proofterm); 
       let _metasenv, _subst, _proofterm, _prooftype = 
         NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
       in
+      prerr_endline "REFINED!";
       ()
   | Failure _ -> prerr_endline "FAILURE";
 ;;