almost complete superposition right step

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 0a7503d12c0e7a678c59629bb5e0dfb68b7ec71d..cf6dcda021130aa471c118cc2e6035425bc7239a 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -17,18 +17,18 @@ foSubst.cmo: terms.cmi foSubst.cmi
 foSubst.cmx: terms.cmx foSubst.cmi 
 orderings.cmo: terms.cmi orderings.cmi 
 orderings.cmx: terms.cmx orderings.cmi 
-foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi 
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
 index.cmo: terms.cmi foUtils.cmi index.cmi 
 index.cmx: terms.cmx foUtils.cmx index.cmi 
 foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
 foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
-superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \
-    foSubst.cmi superposition.cmi 
-superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \
-    foSubst.cmx superposition.cmi 
-nCicBlob.cmo: terms.cmi nCicBlob.cmi 
-nCicBlob.cmx: terms.cmx nCicBlob.cmi 
+superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
+    foUnif.cmi foSubst.cmi superposition.cmi 
+superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
+    foUnif.cmx foSubst.cmx superposition.cmi 
+nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi 
+nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
 paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \

diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index 1dbf27b11bc7a78b9277e2e67ef843c0fb8212fd..cf6dcda021130aa471c118cc2e6035425bc7239a 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -2,9 +2,9 @@ terms.cmi:
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
-foUtils.cmi: terms.cmi index.cmi 
-foUnif.cmi: terms.cmi 
+foUtils.cmi: terms.cmi 
 index.cmi: terms.cmi 
+foUnif.cmi: terms.cmi 
 superposition.cmi: terms.cmi index.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
@@ -17,18 +17,18 @@ foSubst.cmo: terms.cmi foSubst.cmi
 foSubst.cmx: terms.cmx foSubst.cmi 
 orderings.cmo: terms.cmi orderings.cmi 
 orderings.cmx: terms.cmx orderings.cmi 
-foUtils.cmo: terms.cmi orderings.cmi index.cmi foSubst.cmi foUtils.cmi 
-foUtils.cmx: terms.cmx orderings.cmx index.cmx foSubst.cmx foUtils.cmi 
-foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
-foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
+foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
 index.cmo: terms.cmi foUtils.cmi index.cmi 
 index.cmx: terms.cmx foUtils.cmx index.cmi 
-superposition.cmo: terms.cmi orderings.cmi index.cmi foUtils.cmi foUnif.cmi \
-    foSubst.cmi superposition.cmi 
-superposition.cmx: terms.cmx orderings.cmx index.cmx foUtils.cmx foUnif.cmx \
-    foSubst.cmx superposition.cmi 
-nCicBlob.cmo: terms.cmi nCicBlob.cmi 
-nCicBlob.cmx: terms.cmx nCicBlob.cmi 
+foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
+foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
+superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
+    foUnif.cmi foSubst.cmi superposition.cmi 
+superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
+    foUnif.cmx foSubst.cmx superposition.cmi 
+nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi 
+nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 
 cicBlob.cmx: terms.cmx cicBlob.cmi 
 paramod.cmo: superposition.cmi pp.cmi nCicBlob.cmi index.cmi foUtils.cmi \

diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli
index d78ce32f26d49020f4f387833cba41076cfd29a5..3bf04342b11decf81af22a256dbd081326dac0c1 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.mli
+++ b/helm/software/components/ng_paramodulation/foUtils.mli
@@ -29,10 +29,9 @@ module Utils (B : Terms.Blob) :
     val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
     val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
 
-(*
+
     val fresh_unit_clause : 
           int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
-*)
 
     (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
     val relocate : int -> int list -> int * int list * B.t Terms.substitution 

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 6c26e7b86ab82cfeab8996b743d076bd614560f3..3c203d3a7131e7ce1d2411f950975a29c19d9753 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -93,4 +93,6 @@ module Index(B : Terms.Blob) = struct
           DT.index t p (Terms.Nodir, c)
   ;;
 
+  type active_set = B.t Terms.unit_clause list * DT.t
+
 end

diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 5581f7cfa7fd7bbcda4f39d56b00f56b4210c503..5d496d9365f58480ac92c15323624cae9d214284 100644 (file)
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -29,4 +29,6 @@ module Index (B : Terms.Blob) :
     val index_unit_clause :
           DT.t -> B.t Terms.unit_clause -> DT.t 
 
+    type active_set = B.t Terms.unit_clause list * DT.t
+
   end

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index fb93ec7f84edb4d70e3f14c0e0270f2d15ce4545..13b1d7270bc3fd1f785d8831a97ac284ec0b0bce 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -48,8 +48,8 @@ let nparamod metasenv subst context t table =
   in
   prerr_endline "Active table:";
   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
-  let bag, maxvar, newclauses = 
-    Sup.superposition_right_with_table bag maxvar clause table
+  let bag, maxvar, _, newclauses = 
+    Sup.superposition_right bag maxvar clause (active_clauses, table)
   in
   prerr_endline "Output clauses :";
   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 609ca47a7b1a5cce9eff53df81efc39ec71de449..e7353cee8b765af2e7910d3e87101e71d7dd691b 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -86,7 +86,7 @@ let string_of_comparison = function
   | Terms.Incomparable -> "I"
 
 let pp_unit_clause ~formatter:f c =
-  let (id, l, vars, _) = c in
+  let (id, l, vars, proof) = c in
     Format.fprintf f "Id : %d, " id ;
     match l with
       | Terms.Predicate t ->
@@ -98,8 +98,15 @@ let pp_unit_clause ~formatter:f c =
          pp_foterm f lhs;
          Format.fprintf f " =(%s) " (string_of_comparison comp);
          pp_foterm f rhs;
-         Format.fprintf f " [%s]"
-           (String.concat ", " (List.map string_of_int vars))
+         Format.fprintf f " [%s] by %s"
+            (String.concat ", " (List.map string_of_int vars))
+            (match proof with
+            | Terms.Exact _ -> "axiom"
+            | Terms.Step (Terms.SuperpositionRight, id1, id2, _, p, _) -> 
+                 Printf.sprintf "supR %d with %d at %s" id1 id2 (String.concat
+                 "," (List.map string_of_int p))
+            | _ -> assert false)
+
 ;;
 
 (* String buffer implementation *)

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index fe4b578b6c0afc80c91c394c448ebaa3f0677766..6b98ed5be24667a5c6be75049bab6f71ff0de53e 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -130,6 +130,29 @@ module Superposition (B : Terms.Blob) =
                l (superposition_right table vl)))
       | _ -> assert false
     ;;
+
+    (* the current equation is normal w.r.t. demodulation with atable
+     * (and is not the identity) *)
+    let superposition_right bag maxvar current (alist,atable) = 
+      let ctable = IDX.index_unit_clause IDX.DT.empty current in
+      let bag, maxvar, new_clauses =
+        List.fold_left 
+          (fun (bag, maxvar, acc) active ->
+             let bag, maxvar, newc = 
+               superposition_right_with_table bag maxvar active ctable 
+             in
+             bag, maxvar, newc @ acc)
+          (bag, maxvar, []) alist
+      in
+      let alist, atable = 
+        current :: alist, IDX.index_unit_clause atable current
+      in
+      let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
+      let bag, maxvar, additional_new_clauses =
+        superposition_right_with_table bag maxvar fresh_current atable 
+      in
+      bag, maxvar, (alist, atable), new_clauses @ additional_new_clauses
+    ;;
           
   end
 

diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli
index b67233563591d624f42bdaba3e1a2564f6b61e54..54b5ae50f322a031bc926de684e25539c9ec7204 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.mli
+++ b/helm/software/components/ng_paramodulation/superposition.mli
@@ -15,12 +15,13 @@
 module Superposition (B : Terms.Blob) : 
   sig
 
-    val superposition_right_with_table :
+    (* The returned active set is the input one + the selected clause *)
+    val superposition_right :
           B.t Terms.bag -> 
           int -> (* maxvar *)
-          B.t Terms.unit_clause ->
-          Index.Index(B).DT.t ->
-            B.t Terms.bag * int * B.t Terms.unit_clause list
+          B.t Terms.unit_clause -> (* selected *)
+          Index.Index(B).active_set ->
+            B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
                   
   end