Skip to content

Commit

Permalink
Define Shostak printing immediately after type definition (#808)
Browse files Browse the repository at this point in the history 
These functions are useful when debugging and should be defined early so
that they are usable everywhere in the file.
  • Loading branch information
@bclement-ocp
bclement-ocp authored Sep 12, 2023
1 parent e519c30 commit 36e5fe6
Showing 1 changed file with 90 additions and 90 deletions.
180 changes: 90 additions & 90 deletions src/lib/reasoners/shostak.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,96 @@ struct

type r = {v : rview ; id : int}

(*BISECT-IGNORE-BEGIN*)
module Debug = struct
open Printer

let print fmt r =
let open Format in
if Options.get_term_like_pp () then begin
match r.v with
| X1 t -> fprintf fmt "%a" X1.print t
| X2 t -> fprintf fmt "%a" X2.print t
| X3 t -> fprintf fmt "%a" X3.print t
| X4 t -> fprintf fmt "%a" X4.print t
| X5 t -> fprintf fmt "%a" X5.print t
| X6 t -> fprintf fmt "%a" X6.print t
| X7 t -> fprintf fmt "%a" X7.print t
| Term t -> fprintf fmt "%a" Expr.print t
| Ac t -> fprintf fmt "%a" AC.print t
end
else begin
match r.v with
| X1 t -> fprintf fmt "X1(%s):[%a]" X1.name X1.print t
| X2 t -> fprintf fmt "X2(%s):[%a]" X2.name X2.print t
| X3 t -> fprintf fmt "X3(%s):[%a]" X3.name X3.print t
| X4 t -> fprintf fmt "X4(%s):[%a]" X4.name X4.print t
| X5 t -> fprintf fmt "X5(%s):[%a]" X5.name X5.print t
| X6 t -> fprintf fmt "X6(%s):[%a]" X6.name X6.print t
| X7 t -> fprintf fmt "X7(%s):[%a]" X7.name X7.print t
| Term t -> fprintf fmt "FT:[%a]" Expr.print t
| Ac t -> fprintf fmt "Ac:[%a]" AC.print t
end

let print_sbt msg sbs =
let c = ref 0 in
let print fmt (p,v) =
incr c;
Format.fprintf fmt "<%d) %a |-> %a@ "
!c print p print v
in
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"print_sbt"
"@[<v 2>%s subst:@ %a@]"
msg
(pp_list_no_space print) sbs

let debug_abstraction_result oa ob a b acc =
let c = ref 0 in
let print fmt (p,v) =
incr c;
Format.fprintf fmt "(%d) %a |-> %a@ "
!c CX.print p CX.print v
in
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"abstraction_result"
"@[<v 0>== get_debug_abstraction_result ==@ \
Initial equaliy: %a = %a@ \
abstracted equality: %a = %a@ \
@[<v 2>selectors elimination result:@ \
%a@]@]"
CX.print oa CX.print ob CX.print a CX.print b
(pp_list_no_space print) acc

let solve_one a b =
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"solve_one"
"solve one %a = %a" CX.print a CX.print b

let debug_abstract_selectors a =
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"abstract_selectors"
"abstract selectors of %a" CX.print a

let assert_have_mem_types tya tyb =
assert (
not (Options.get_enable_assertions()) ||
if not (Ty.compare tya tyb = 0) then (
print_err "@[<v 0>@ Tya = %a and @ Tyb = %a@]"
Ty.print tya Ty.print tyb;
false)
else true)

end
(*BISECT-IGNORE-END*)

let print = Debug.print


(* begin: Hashconsing modules and functions *)

module View = struct
Expand Down Expand Up @@ -365,96 +455,6 @@ struct
| false , false , false , false, false, false, true , false -> X7.color ac
| _ -> ac_embed ac


(*BISECT-IGNORE-BEGIN*)
module Debug = struct
open Printer

let print fmt r =
let open Format in
if Options.get_term_like_pp () then begin
match r.v with
| X1 t -> fprintf fmt "%a" X1.print t
| X2 t -> fprintf fmt "%a" X2.print t
| X3 t -> fprintf fmt "%a" X3.print t
| X4 t -> fprintf fmt "%a" X4.print t
| X5 t -> fprintf fmt "%a" X5.print t
| X6 t -> fprintf fmt "%a" X6.print t
| X7 t -> fprintf fmt "%a" X7.print t
| Term t -> fprintf fmt "%a" Expr.print t
| Ac t -> fprintf fmt "%a" AC.print t
end
else begin
match r.v with
| X1 t -> fprintf fmt "X1(%s):[%a]" X1.name X1.print t
| X2 t -> fprintf fmt "X2(%s):[%a]" X2.name X2.print t
| X3 t -> fprintf fmt "X3(%s):[%a]" X3.name X3.print t
| X4 t -> fprintf fmt "X4(%s):[%a]" X4.name X4.print t
| X5 t -> fprintf fmt "X5(%s):[%a]" X5.name X5.print t
| X6 t -> fprintf fmt "X6(%s):[%a]" X6.name X6.print t
| X7 t -> fprintf fmt "X7(%s):[%a]" X7.name X7.print t
| Term t -> fprintf fmt "FT:[%a]" Expr.print t
| Ac t -> fprintf fmt "Ac:[%a]" AC.print t
end

let print_sbt msg sbs =
let c = ref 0 in
let print fmt (p,v) =
incr c;
Format.fprintf fmt "<%d) %a |-> %a@ "
!c print p print v
in
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"print_sbt"
"@[<v 2>%s subst:@ %a@]"
msg
(pp_list_no_space print) sbs

let debug_abstraction_result oa ob a b acc =
let c = ref 0 in
let print fmt (p,v) =
incr c;
Format.fprintf fmt "(%d) %a |-> %a@ "
!c CX.print p CX.print v
in
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"abstraction_result"
"@[<v 0>== get_debug_abstraction_result ==@ \
Initial equaliy: %a = %a@ \
abstracted equality: %a = %a@ \
@[<v 2>selectors elimination result:@ \
%a@]@]"
CX.print oa CX.print ob CX.print a CX.print b
(pp_list_no_space print) acc

let solve_one a b =
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"solve_one"
"solve one %a = %a" CX.print a CX.print b

let debug_abstract_selectors a =
if Options.get_debug_combine () then
print_dbg
~module_name:"Shostak" ~function_name:"abstract_selectors"
"abstract selectors of %a" CX.print a

let assert_have_mem_types tya tyb =
assert (
not (Options.get_enable_assertions()) ||
if not (Ty.compare tya tyb = 0) then (
print_err "@[<v 0>@ Tya = %a and @ Tyb = %a@]"
Ty.print tya Ty.print tyb;
false)
else true)

end
(*BISECT-IGNORE-END*)

let print = Debug.print

let abstract_selectors a acc =
Debug.debug_abstract_selectors a;
match a.v with
Expand Down

0 comments on commit 36e5fe6

Please sign in to comment.