From 04964c70f5afd95d66fc76945e62dce773a3b3bc Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 16 Feb 2022 10:38:15 +0100 Subject: Add debugging information for uninterpreted functions --- src/trace/satAtom.ml | 2 +- src/trace/satAtom.mli | 2 +- src/trace/smtAtom.ml | 14 ++++++++------ src/trace/smtAtom.mli | 2 +- src/trace/smtForm.ml | 20 ++++++++++---------- src/trace/smtForm.mli | 2 +- 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 -- cgit