]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/superposition.ml
Various fixes
[helm.git] / helm / software / components / ng_paramodulation / superposition.ml
index 891c8dcacafaec6553e6884983448838fab7da1e..8e77936c8f964bc721b64170a3326ce1db3e3890 100644 (file)
@@ -178,12 +178,13 @@ module Superposition (B : Terms.Blob) =
     ;;
 
     (* move away *)
-    let is_identity_clause = function
+    let is_identity_clause ~unify = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Equation (l,r,_,_), vl, proof ->
+      | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
          (try ignore(Unif.unification vl [] l r); true
          with FoUnif.UnificationFailure _ -> false)
       | _, Terms.Predicate _, _, _ -> assert false       
+      | _ -> false
     ;;
 
     let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =
@@ -205,63 +206,85 @@ module Superposition (B : Terms.Blob) =
        bag, maxvar, res
     ;;
 
+    
+    let rewrite_eq ~unify l r ty vl table =
+      let retrieve = if unify then IDX.DT.retrieve_unifiables
+      else IDX.DT.retrieve_generalizations in
+      let lcands = retrieve table l in
+      let rcands = retrieve table r in
+      let f b c = 
+        let id, dir, l, r, vl = 
+          match c with
+            | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
+            |_ -> assert false 
+        in 
+       let reverse = (dir = Terms.Left2Right) = b in
+        let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
+       else r,l, Terms.Right2Left in
+          (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
+      in
+      let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
+      let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
+      let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
+      let locked_vars = if unify then [] else vl in
+      let rec aux = function
+       | [] -> None
+       | (id2,dir,c,vl1)::tl ->
+           try
+             let subst,vl1 = Unif.unification (vl@vl1) locked_vars c t in
+              Some (id2, dir, subst)
+           with FoUnif.UnificationFailure _ -> aux tl
+      in
+       aux (cands1 @ cands2)
+    ;;
+
     let is_subsumed ~unify bag maxvar (id, lit, vl, _) table =
       match lit with
       | Terms.Predicate _ -> assert false
       | Terms.Equation (l,r,ty,_) -> 
-         let retrieve = if unify then IDX.DT.retrieve_unifiables
-         else IDX.DT.retrieve_generalizations in
-          let lcands = retrieve table l in
-          let rcands = retrieve table r in
-          let f b c = 
-            let id, dir, l, r, vl = 
-              match c with
-              | (d, (id,Terms.Equation (l,r,ty,_),vl,_))-> id, d, l, r, vl
-              |_ -> assert false 
-            in 
-           let reverse = (dir = Terms.Left2Right) = b in
-            let l, r, proof_rewrite_dir = if reverse then l,r,Terms.Left2Right
-           else r,l, Terms.Right2Left in
-            (id,proof_rewrite_dir,Terms.Node [ Terms.Leaf B.eqP; ty; l; r ], vl)
-          in
-          let cands1 = List.map (f true) (IDX.ClauseSet.elements lcands) in
-          let cands2 = List.map (f false) (IDX.ClauseSet.elements rcands) in
-          let t = Terms.Node [ Terms.Leaf B.eqP; ty; l; r ] in
-         let locked_vars = if unify then [] else vl in
-         let rec aux = function
-           | [] -> None
-           | (id2,dir,c,vl1)::tl ->
-               try
-                 let subst,vl1 = Unif.unification (vl@vl1) locked_vars c t in
-                 let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
-                   build_new_clause bag maxvar (fun _ -> true)
-                     Terms.Superposition id_t subst [] id id2 [2] dir 
-               with FoUnif.UnificationFailure _ -> aux tl
-         in
-           aux (cands1 @ cands2)
+          match rewrite_eq ~unify l r ty vl table with
+           | None -> None
+           | Some (id2, dir, subst) ->
+               let id_t = Terms.Node [ Terms.Leaf B.eqP; ty; r; r ] in
+                 build_new_clause bag maxvar (fun _ -> true)
+                   Terms.Superposition id_t subst [] id id2 [2] dir 
     ;;
 
+(*
+    let rec deeply_subsumed ~unify bag maxvar (id, lit, vl, _) table =
+      match lit with
+      | Terms.Predicate _ -> assert false
+      | Terms.Equation (l,r,ty,_) -> 
+       (match is_subsumed ~unify bag maxvar (id, lit, vl, _) table with
+        | Some((bag,maxvar),c) -> Some((bag,maxvar),c)
+        | None -> 
+            match l,r with ->
+              Var i, _ -> 
+    ;;
+*)       
+
+
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       let bag, clause = demodulate bag clause table in
-      if is_identity_clause clause then None
+      if is_identity_clause ~unify:false clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
-         | None -> Some (bag, clause)
-         | Some _ -> None
+         | None -> bag, Some clause
+         | Some _ -> bag, None
     ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
-       | None -> None (* new_clause has been discarded *)
-       | Some (bag, clause) ->
+       | bag,None -> None (* new_clause has been discarded *)
+       | bag,(Some 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 maxvar bag c with
-                    |None -> acc (* an active clause as been discarded *)
-                    |Some (bag, c1) ->
+                    |bag,None -> acc (* an active clause as been discarded *)
+                    |bag,Some c1 ->
                        bag, c :: alist, IDX.index_unit_clause atable c)
                (bag,[],IDX.DT.empty) alist
            in
@@ -277,8 +300,8 @@ module Superposition (B : Terms.Blob) =
         * - actives and cl if new_clause is not cl *
         * - only actives otherwise                 *)
        match simplify atable1 maxvar bag new_clause with
-         | None -> (Some cl, None) (* new_clause has been discarded *)
-         | Some (bag, clause) ->
+         | bag,None -> (Some cl, None) (* new_clause has been discarded *)
+         | bag,Some 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
@@ -286,8 +309,8 @@ module Superposition (B : Terms.Blob) =
                List.fold_left 
                  (fun (bag, newa, alist, atable as acc) c ->
                     match simplify ctable maxvar bag c with
-                      |None -> acc (* an active clause as been discarded *)
-                      |Some (bag, c1) ->
+                      |bag,None -> acc (* an active clause as been discarded *)
+                      |bag,Some c1 ->
                            if (c1 == c) then 
                              bag, newa, c :: alist,
                            IDX.index_unit_clause atable c
@@ -300,10 +323,10 @@ module Superposition (B : Terms.Blob) =
                else
                  (* if new_clause is not cl, we simplify cl with clause *)
                  match simplify ctable maxvar bag cl with
-                   | None ->
+                   | bag,None ->
                        (* cl has been discarded *)
                        (None, Some (clause, (alist,atable), newa, bag))
-                   | Some (bag,cl1) ->
+                   | bag,Some cl1 ->
                        (Some cl1, Some (clause, (alist,atable), newa, bag))
     ;;
 
@@ -350,7 +373,7 @@ module Superposition (B : Terms.Blob) =
     (* this is like simplify but raises Success *)
     let simplify_goal maxvar table bag g_actives clause = 
       let bag, clause = demodulate bag clause table in
-      if (is_identity_clause clause)
+      if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
       else match is_subsumed ~unify:true bag maxvar clause table with
        | None -> 
@@ -469,7 +492,7 @@ module Superposition (B : Terms.Blob) =
        debug (Printf.sprintf "Demodulating %d clauses"
                 (List.length new_clauses));
       let bag, new_clauses = 
-        HExtlib.filter_map_acc (simplify atable maxvar) bag new_clauses
+        HExtlib.filter_map_monad (simplify atable maxvar) bag new_clauses
       in
        debug "Demodulated new clauses";
       bag, maxvar, (alist, atable), new_clauses