aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.ml
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2022-02-17 10:50:50 +0100
committerChantal Keller <Chantal.Keller@lri.fr>2022-02-17 10:50:50 +0100
commit55d2990e9bf607c3c2f75bf98348bee19de03656 (patch)
treec2ae4efb81726c35f2f66440d370cb53e096eeb8 /src/trace/smtAtom.ml
parent23ac3ceceb92cdbc2026253c1bae388a2b9b6e18 (diff)
parentbf51e8a18116d3f2f340d3be0444c7e15b2c21cb (diff)
downloadsmtcoq-55d2990e9bf607c3c2f75bf98348bee19de03656.tar.gz
smtcoq-55d2990e9bf607c3c2f75bf98348bee19de03656.zip
Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12
Diffstat (limited to 'src/trace/smtAtom.ml')
-rw-r--r--src/trace/smtAtom.ml16
1 files changed, 9 insertions, 7 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 6447ae7..ccd9629 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 *)
(* *)
@@ -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