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(-) (limited to 'src/trace') 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 From 2fdaf566e83897ed46127791d731f5788c22907c Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 16 Feb 2022 17:35:44 +0100 Subject: Update copyright --- src/trace/coqTerms.ml | 2 +- src/trace/coqTerms.mli | 2 +- src/trace/satAtom.ml | 2 +- src/trace/satAtom.mli | 2 +- src/trace/smtAtom.ml | 2 +- src/trace/smtAtom.mli | 2 +- src/trace/smtBtype.ml | 2 +- src/trace/smtBtype.mli | 2 +- src/trace/smtCertif.ml | 2 +- src/trace/smtCertif.mli | 2 +- src/trace/smtCnf.ml | 2 +- src/trace/smtCnf.mli | 2 +- src/trace/smtCommands.ml | 2 +- src/trace/smtCommands.mli | 2 +- src/trace/smtForm.ml | 2 +- src/trace/smtForm.mli | 2 +- src/trace/smtMaps.ml | 2 +- src/trace/smtMaps.mli | 2 +- src/trace/smtMisc.ml | 2 +- src/trace/smtMisc.mli | 2 +- src/trace/smtTrace.ml | 2 +- src/trace/smtTrace.mli | 2 +- 22 files changed, 22 insertions(+), 22 deletions(-) (limited to 'src/trace') diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 65995b5..dcacd4b 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 282f8f6..f62f01a 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 6ffd752..4a3a62d 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index b6a8dea..1e14cbb 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 06e1472..1befbf7 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 645a638..b430d6f 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 7c08157..71f7c14 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index ec73d21..05a8486 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 2ea4ca8..33437bf 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli index 7da3097..ef25b1f 100644 --- a/src/trace/smtCertif.mli +++ b/src/trace/smtCertif.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml index c7601d5..ffd2c45 100644 --- a/src/trace/smtCnf.ml +++ b/src/trace/smtCnf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli index ba9be04..b15eef7 100644 --- a/src/trace/smtCnf.mli +++ b/src/trace/smtCnf.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 9cfc7c4..d15ae68 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index b643594..eddf576 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index a86fe8a..6f26f24 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index e3c3859..9678b4c 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMaps.ml b/src/trace/smtMaps.ml index 8b1bc9f..df87579 100644 --- a/src/trace/smtMaps.ml +++ b/src/trace/smtMaps.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMaps.mli b/src/trace/smtMaps.mli index 220b22a..ebbdc64 100644 --- a/src/trace/smtMaps.mli +++ b/src/trace/smtMaps.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index e4747dd..227f2ff 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index 6378627..149e377 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index 876e420..e637b5c 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index 2c70bbc..06dc6a3 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* SMTCoq *) -(* Copyright (C) 2011 - 2021 *) +(* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) -- cgit