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/smtForm.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'src/trace/smtForm.ml') 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 = -- 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/smtForm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/trace/smtForm.ml') 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 *) (* *) -- cgit