]> matita.cs.unibo.it Git - helm.git/commitdiff
goal demodulated with new
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 May 2006 15:15:47 +0000 (15:15 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 May 2006 15:15:47 +0000 (15:15 +0000)
components/tactics/paramodulation/equality.ml
components/tactics/paramodulation/equality.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/saturation.ml

index 6c0b24327d6fca5dcedc1a0417d8f6caa8999056..c4aaa1ca485979031e2b7ad434e8c5783eb4d3f6 100644 (file)
@@ -264,6 +264,12 @@ let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
   eq
 ;;
 
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+  let id = -1 in
+  uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id
+;;
+
+
 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
   (weight,proof,(ty,l,r,o),m,id)
 
@@ -706,7 +712,7 @@ let wfo goalproof =
   let rec aux acc id =
     let p,_,_ = proof_of_id id in
     match p with
-    | Exact _ -> id :: acc
+    | Exact _ -> if (List.mem id acc) then acc else id :: acc
     | Step (_,(_,id1, (_,id2), _)) -> 
         let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
         let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
@@ -723,14 +729,18 @@ let string_of_id names id =
         Printf.sprintf "%d = %s: %s = %s" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
     | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%5d: %s %4d %4d   %s = %s" id
+        Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
           (if step = SuperpositionRight then "SupR" else "Demo") 
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
   with
       Not_found -> assert false
 
 let pp_proof names goalproof =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof))
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof)) ^ 
+  "\ngoal is demodulated with " ^ 
+    (String.concat " " 
+      ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
 
 let build_goal_proof l initial =
   let proof = 
index ea0cefd55113dca76d0f48b236246a2363fbdc2e..2d7e48e5cb13dd18ba66d6f0f7543622630b26e3 100644 (file)
@@ -70,6 +70,10 @@ val mk_equality :
   (Cic.term * Cic.term * Cic.term * Utils.comparison) *
   Cic.metasenv -> 
     equality
+
+val mk_tmp_equality :
+  int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv -> 
+    equality
     
 val open_equality :
   equality ->
index 584bf5c60950c684eeda9e250d00c2c9487c5994..4ac1c94e29f12a0f93a22f085d5a75ca94f19068 100644 (file)
@@ -639,7 +639,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
       in
       if sign = Utils.Positive then
           (bo,
-           (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+           (Equality.Step (subst,(Equality.Demodulation,
+             id,(pos,id'),
                         (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
            Equality.ProofBlock (
              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
@@ -750,7 +751,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality newmeta env table sign newtarget
+            demodulation_equality ?from newmeta env table sign newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -761,7 +762,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality newmeta env table sign newtarget
+                   demodulation_equality ?from newmeta env table sign newtarget
           | None ->
               newmeta, target
   in
@@ -1066,8 +1067,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       (* qua *)
-      let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
-(*      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+      let bo' =
+        Utils.guarded_simpl context (apply_subst s (S.subst other bo)) 
+      in
       let name = C.Name "x" in
       incr sup_r_counter;
       let bo'' =
@@ -1077,9 +1079,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                 S.lift 1 eq_ty; l; r]
       in
       bo',
-      ( Equality.Step (s,(Equality.SuperpositionRight,
-                     id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
-       Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+      (Equality.Step 
+        (s,(Equality.SuperpositionRight,
+           id,(pos,id'),(Cic.Lambda(name,ty,bo'')))),
+       Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
        
     in
     let newmeta, newequality = 
index f1cec900f1d54eaa100f1a0f8006d490c9bc176b..1cb6d351433f158a52aa5511b51e0c36c32b1bd1 100644 (file)
@@ -354,6 +354,50 @@ let infer env current (active_list, active_table) =
         List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 ;;
 
+let check_for_deep_subsumption env active_table eq =
+  let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
+  if id = 14242 then assert false;
+  
+  let check deep l r = 
+    let eqtmp = 
+      Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
+    match Indexing.subsumption env active_table eqtmp with
+    | None -> false
+    | Some (s,eq') -> 
+        prerr_endline 
+          ("\n\n " ^ Equality.string_of_equality ~env eq ^ 
+          "\nis"^(if deep then " CONTEXTUALLY " else " ")^"subsumed by \n " ^ 
+          Equality.string_of_equality ~env eq' ^ "\n\n");
+        true        
+  in 
+  let rec aux b = function
+    | Cic.Rel n, Cic.Rel m -> if n = m then true else false
+    | ((Cic.Appl l) as left),((Cic.Appl l') as right) ->
+        check b left right ||
+        (try 
+          List.for_all2 (fun t t' -> aux true (t,t')) (List.tl l) (List.tl l')
+        with Invalid_argument _ -> false)
+    | (Cic.Meta _),_ 
+    | _,(Cic.Meta _) -> false
+    | _ -> false
+  in
+  aux false (left,right)
+;;
+
+(*
+let check_for_deep env active_table eq =
+  match Indexing.subsumption env active_table eq with
+  | None -> false
+  | Some _ -> true
+;;
+*)
+
+let profiler = HExtlib.profile "check_for_deep";;
+
+let check_for_deep_subsumption env active_table eq = 
+  profiler.HExtlib.profile (check_for_deep_subsumption env active_table) eq
+;;
+
 (* buttare via sign *)
 
 (** simplifies current using active and passive *)
@@ -407,26 +451,35 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
   match res with
   | None -> None
   | Some c ->
-      (* immagino non funzioni piu'... *)
       if Indexing.in_index active_table c then
         None
       else
         match passive_table with
         | None -> 
+            if check_for_deep_subsumption env active_table c then
+              None
+            else 
+              res
+(*
             if Indexing.subsumption env active_table c = None then
               res
             else
               None
+*)
         | Some passive_table ->
             if Indexing.in_index passive_table c then None
             else 
-              if Indexing.subsumption env active_table c = None then
-                if Indexing.subsumption env passive_table c = None then
-                  res 
-                else
-                  None
+              if check_for_deep_subsumption env active_table c then
+                None
+              else 
+(*              if Indexing.subsumption env active_table c = None then*)
+                (match Indexing.subsumption env passive_table c with
+                | None -> res
+                | Some (_,c') -> None (*Some c'*))
+(*
               else
                 None
+*)
 ;;
 
 type fs_time_info_t = {
@@ -525,8 +578,8 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
     | None -> demodulate active_table goal
     | Some passive_table ->
         let changed, goal = demodulate active_table goal in
-        let changed', goal = demodulate passive_table goal in
-        (changed || changed'), goal
+(*        let changed', goal = demodulate passive_table goal in*)
+        (changed (*|| changed'*)), goal
   in
   changed,
   if not changed then 
@@ -634,15 +687,25 @@ let backward_simplify_passive env new_pos new_table min_weight passive =
   |  _ -> ((pl, ps), passive_table), Some (newp)
 ;;
 
+let build_table equations =
+    List.fold_left
+      (fun (l, t, w) e ->
+         let ew, _, _, _ , _ = Equality.open_equality e in
+         e::l, Indexing.index t e, min ew w)
+      ([], Indexing.empty, 1000000) equations
+;;
+  
 
 let backward_simplify env new' ?passive active =
-  let new_pos, new_table, min_weight =
+  let new_pos, new_table, min_weight = build_table new' in
+(*
     List.fold_left
       (fun (l, t, w) e ->
          let ew, _, _, _ , _ = Equality.open_equality e in
          e::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) new'
   in
+*)
   let active, newa =
     backward_simplify_active env new_pos new_table min_weight active in
   match passive with
@@ -1103,6 +1166,11 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                   simplify (new' @ p @ rp) active passive
             in
             let active, _, new' = simplify new' active passive in
+            let goals = 
+              let a,b,_ = build_table new' in
+              simplify_goals env goals ~passive (a,b)
+            in
+              
 (* pessima prova 
             let new1 = prova env new' active in
             let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in