almost complete superposition right step

[helm.git] / helm / software / components / ng_paramodulation / pp.ml

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 *)