Add debugging information for uninterpreted functions

6 files changed, 22 insertions, 20 deletions

diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index ff648a9..bc59943 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -55,7 +55,7 @@ module Atom =
 
     let logic _ = SL.empty
 
-    let to_smt = Format.pp_print_int
+    let to_smt ?(debug=false) = Format.pp_print_int
     
   end
 
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 311b147..875e1ad 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -18,7 +18,7 @@ module Atom : sig
 
   val is_bool_type : t -> bool
   val is_bv_type : t -> bool
-  val to_smt : Format.formatter -> t -> unit
+  val to_smt : ?debug:bool -> Format.formatter -> t -> unit
   val logic : t -> SmtMisc.logic
 
   type reify_tbl = {
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 6447ae7..23c56e7 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -707,12 +707,12 @@ module Atom =
       | [] -> ()
 
 
-    let to_smt_named ?pi:(pi=false) (fmt:Format.formatter) h =
+    let to_smt_named ?(debug=false) ?pi:(pi=false) (fmt:Format.formatter) h =
       let rec to_smt fmt h =
         if pi then Format.fprintf fmt "%d:" (index h);
-        to_smt_atom (atom h)
+        to_smt_atom ~debug:debug (atom h)
 
-      and to_smt_atom = function
+      and to_smt_atom ?(debug=false) = function
         | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
         | Acop _ as a -> to_smt_int fmt (compute_int a)
         | Auop (op,h) -> to_smt_uop op h
@@ -722,7 +722,9 @@ module Atom =
         | Aapp ((i,op),a) ->
            let op_smt () =
              (match i with
-                | Index index -> Format.fprintf fmt "op_%i" index
+                | Index index ->
+                   (Format.fprintf fmt "op_%i" index;
+                    if debug then Format.fprintf fmt " (aka %s)" (Pp.string_of_ppcmds (CoqInterface.pr_constr op.op_val));)
                 | Rel_name name -> Format.fprintf fmt "%s" name);
              if pi then to_smt_op op
            in
@@ -805,7 +807,7 @@ module Atom =
       in
       to_smt fmt h
 
-    let to_smt (fmt:Format.formatter) h = to_smt_named fmt h
+    let to_smt ?(debug=false) (fmt:Format.formatter) h = to_smt_named ~debug:debug fmt h
 
 
     type reify_tbl =
@@ -855,7 +857,7 @@ module Atom =
         else (
           Format.eprintf "Incorrect type: wanted %a, got %a@."
             SmtBtype.to_smt t SmtBtype.to_smt th;
-          failwith (Format.asprintf "Atom %a is not of the expected type" to_smt h)
+          failwith (Format.asprintf "Atom %a is not of the expected type" (to_smt ~debug:true) h)
         )
       in
 
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 27737ff..05d4042 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -119,7 +119,7 @@ module Atom :
 
       val type_of : t -> btype
 
-      val to_smt : Format.formatter -> t -> unit
+      val to_smt : ?debug:bool -> Format.formatter -> t -> unit
 
       type reify_tbl
 
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 0a5f693..8019f3b 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -25,7 +25,7 @@ module type ATOM =
 
     val is_bool_type : t -> bool
     val is_bv_type : t -> bool
-    val to_smt : Format.formatter -> t -> unit
+    val to_smt : ?debug:bool -> Format.formatter -> t -> unit
     val logic : t -> logic
 
   end
@@ -173,12 +173,12 @@ module Make (Atom:ATOM) =
          to_smt_pform fmt hp.hval;
          Format.fprintf fmt ")"
 
-    and to_smt_pform fmt = function
-      | Fatom a -> Atom.to_smt fmt a
+    and to_smt_pform ?(debug=false) fmt = function
+      | Fatom a -> Atom.to_smt ~debug:debug fmt a
       | Fapp (op,args) -> to_smt_op fmt op args
       (* This is an intermediate object of proofs, it correspond to nothing in SMT *)
       | FbbT (a, l) ->
-        Format.fprintf fmt "(bbT %a [" Atom.to_smt a;
+        Format.fprintf fmt "(bbT %a [" (Atom.to_smt ~debug:debug) a;
         let fi = ref true in
         List.iter (fun f -> Format.fprintf fmt "%s%a"
                       (if !fi then "" else "; ")
@@ -296,34 +296,34 @@ module Make (Atom:ATOM) =
     let check pf =
       match pf with
       | Fatom ha ->  if not (Atom.is_bool_type ha) then
-          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+          raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                  NotWellTyped pf)
       | Fapp (op, args) ->
 	(match op with
 	 | Ftrue | Ffalse ->
            if Array.length args <> 0 then
-             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+             raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                     NotWellTyped pf)
 	 | Fnot2 _ ->
            if Array.length args <> 1 then
-             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+             raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                     NotWellTyped pf)
 	 | Fand | For -> ()
 	 | Fxor | Fimp | Fiff ->
            if Array.length args <> 2 then
-             raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+             raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                     NotWellTyped pf)
 
           | Fite ->
             if Array.length args <> 3 then
-              raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+              raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                      NotWellTyped pf)
 
          | Fforall l -> ()
        )
 
       | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then
-          raise (Format.eprintf "nwt: %a" to_smt_pform pf;
+          raise (Format.eprintf "nwt: %a" (to_smt_pform ~debug:true) pf;
                  NotWellTyped pf)
 
     let declare reify pf =
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index 47b4123..560b9e4 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -22,7 +22,7 @@ module type ATOM =
 
     val is_bool_type : t -> bool
     val is_bv_type : t -> bool
-    val to_smt : Format.formatter -> t -> unit
+    val to_smt : ?debug:bool -> Format.formatter -> t -> unit
     val logic : t -> logic
 
   end