Fixed a few bugs

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 781b6bf08316b42efbff3365fe47c3eb8a919333..df6f949b603c867128b5d31634cf72091199ab9e 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -207,7 +207,7 @@ let debug c _ = c;;
               List.fold_left
                (fun (i,acc) t ->
                  i+1,
-                             let f = extract amount vl f in
+                      let f = extract amount vl f in
                   if i = n then
                    let imp = NCic.Implicit `Term in
                     NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
@@ -218,7 +218,7 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  (* we should better split forward and backard rewriting *)
+  (* we should better split forward and backward rewriting *)
   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
     let module NCicBlob = 
        NCicBlob.NCicBlob(
@@ -264,6 +264,26 @@ let debug c _ = c;;
       let lit,_,_ = get_literal mp in
       let lit = Subst.apply_subst subst lit in
         extract 0 [] lit in
+    (* composition of all subst acting on goal *)
+    let res_subst =
+      let rec rsaux ongoal acc = 
+       function
+         | [] -> acc (* is the final subst for refl *)
+         | id::tl when ongoal ->
+            let lit,vl,proof = get_literal id in
+             (match proof with
+               | Terms.Exact _ -> rsaux ongoal acc tl
+               | Terms.Step (_, _, _, _, _, s) ->
+                   rsaux ongoal (s@acc) tl)
+         | id::tl -> 
+           (* subst is the the substitution for refl *)
+           rsaux (id=mp) subst tl
+      in 
+      let r = rsaux false [] steps in
+       (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
+           prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
+      r
+    in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
@@ -305,10 +325,12 @@ let debug c _ = c;;
               let id, id1,(lit,vl,proof) =
                 if ongoal then
                  let lit,vl,proof = get_literal id1 in
-                 id1,id,(Subst.apply_subst subst lit, 
-                         Subst.filter subst vl, proof)
+                 id1,id,(Subst.apply_subst res_subst lit, 
+                         Subst.filter res_subst vl, proof)
                 else id,id1,(lit,vl,proof) in
-              let vl = if ongoal then [] else vl in
+              (* free variables remaining in the goal should not
+                 be abstracted: we do not want to prove a generalization *)
+              let vl = if ongoal then [] else vl in 
               let proof_of_id id = 
                 let vars = List.rev (vars_of id seen) in
                 let args = List.map (Subst.apply_subst subst) vars in
@@ -388,7 +410,8 @@ let debug c _ = c;;
               let body = aux ongoal 
                 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl 
               in 
-                if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+             let occ= NCicUntrusted.count_occurrences [] 1 body in
+               if occ <= 1 then
                   NCicSubstitution.subst 
                     ~avoid_beta_redexes:true ~no_implicit:false
                     (close_with_lambdas vl rewrite_step) body

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index de32ab5ddf8b7e0fe1b8984ed4bdad4e4d4c3970..7fc13b504290aebbf11bbcfbf5032131ce60ad7d 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -202,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
@@ -210,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 *)
@@ -268,7 +276,7 @@ module Paramod (B : Orderings.Blob) = struct
        (List.map Pp.pp_unit_clause actives_l)))
       ^ 
       ("Passives:" ^(String.concat ";\n" 
-        (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+        (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
               (IDX.ClauseSet.elements wset))))
   ;;
 
@@ -287,7 +295,7 @@ 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)))));
-    debug (lazy (pp_clauses actives passives));
+    noprint (lazy (pp_clauses actives passives));
     match Sup.keep_simplified current actives bag maxvar
     with
       | _,None -> s
@@ -356,7 +364,7 @@ module Paramod (B : Orderings.Blob) = struct
     let _ = noprint
       (lazy 
         ("Passives:" ^(String.concat ";\n" 
-           (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+           (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
               (IDX.ClauseSet.elements wset))))) in 
     let g_passives = 
       WeightPassiveSet.fold 
@@ -566,7 +574,7 @@ let demod s goal =
 
 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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index f38acb536a707eeb5d0871b781af25cd2af412eb..c5bb640a2ba8bdb5c532f7bcf89a3686c0c29fa9 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -412,6 +412,7 @@ module Superposition (B : Orderings.Blob) =
       match acc with 
       | None -> None
       | Some(bag,maxvar,(id,lit,vl,p),subst) -> 
+          (* prerr_endline ("input subst = "^Pp.pp_substitution subst); *)
           let l = Subst.apply_subst subst l in 
           let r = Subst.apply_subst subst r in 
             try 
@@ -426,6 +427,8 @@ module Superposition (B : Orderings.Blob) =
             with FoUnif.UnificationFailure _ -> 
               match rewrite_eq ~unify l r ty vl table with
               | Some (id2, dir, subst1) ->
+                 (* prerr_endline ("subst1 = "^Pp.pp_substitution subst1);
+                    prerr_endline ("old subst = "^Pp.pp_substitution subst);*)
                   let newsubst = Subst.concat subst1 subst in
                   let id_t = 
                     FoSubst.apply_subst newsubst
@@ -437,7 +440,9 @@ module Superposition (B : Orderings.Blob) =
                         subst1 id id2 (pos@[2]) dir 
                     with
                     | Some ((bag, maxvar), c), r ->
-                       let newsubst = Subst.concat r newsubst in
+                       (* prerr_endline ("r = "^Pp.pp_substitution r); *)
+                       let newsubst = Subst.flat 
+                         (Subst.concat r subst) in
                         Some(bag,maxvar,c,newsubst)
                     | None, _ -> assert false)
               | None ->