Skip to content

Commit

Permalink
better printer
Browse files Browse the repository at this point in the history
  • Loading branch information
@Halbaroth
Halbaroth committed Oct 29, 2024
1 parent 35c0f14 commit 83f5ca9
Show file tree
Hide file tree
Showing 10 changed files with 449 additions and 166 deletions.
27 changes: 12 additions & 15 deletions src/lib/reasoners/adt.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,20 +105,23 @@ module Shostak (X : ALIEN) = struct
| Some c -> c
| None -> Alien r

let pp_field ppf (lbl, v) =
Fmt.pf ppf "%a : %a" DE.Term.Const.print lbl X.print v

let print ppf = function
| Alien x ->
X.print ppf x

| Constr { c_name; c_args; _ } ->
Fmt.pf ppf "%a@[(%a@])"
DE.Term.Const.print c_name
Fmt.(list ~sep:semi pp_field) c_args
if Compat.List.is_empty c_args then
Fmt.pf ppf "%a"
(Fmt.styled (`Fg `Blue) DE.Term.Const.print) c_name
else
Fmt.pf ppf "(%a %a)"
(Fmt.styled (`Fg `Blue) DE.Term.Const.print) c_name
Fmt.(list ~sep:sp @@ pair nop X.print) c_args

| Select d ->
Fmt.pf ppf "%a#!!%a" X.print d.d_arg DE.Term.Const.print d.d_name
Fmt.pf ppf "(%a %a)"
X.print d.d_arg
(Fmt.styled (`Fg `Red) DE.Term.Const.print) d.d_name


let is_mine u =
Expand Down Expand Up @@ -168,10 +171,7 @@ module Shostak (X : ALIEN) = struct

let make t =
assert (not @@ Options.get_disable_adts ());
if Options.get_debug_adt () then
Printer.print_dbg
~module_name:"Adt" ~function_name:"make"
"make %a" E.print t;
Log.debug (fun k -> k"make@ '%a'" E.pp_debug t);
let { E.f; xs; ty; _ } = E.term_view t in
let sx, ctx =
List.fold_left
Expand Down Expand Up @@ -360,10 +360,7 @@ module Shostak (X : ALIEN) = struct
List.exists (fun y -> X.equal x y) (X.leaves e)

let solve r1 r2 pb =
if Options.get_debug_adt () then
Printer.print_dbg
~module_name:"Adt" ~function_name:"solve"
"solve %a = %a" X.print r1 X.print r2;
Log.debug (fun k -> k "solve:@ '%a' = '%a'" X.print r1 X.print r2);
assert (not @@ Options.get_disable_adts ());
match embed r1, embed r2 with
| Select _, _ | _, Select _ -> assert false (* should be eliminated *)
Expand Down
24 changes: 16 additions & 8 deletions src/lib/reasoners/adt_rel.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -111,11 +111,19 @@ module Domain = struct

let equal d1 d2 = TSet.equal d1.constrs d2.constrs

let pp_constrs ppf constrs =
Fmt.(box @@ braces
@@ iter ~sep:comma TSet.iter
@@ styled (`Fg `Blue)
@@ DE.Term.Const.print) ppf constrs

let pp ppf d =
Fmt.(braces @@
iter ~sep:comma TSet.iter DE.Term.Const.print) ppf d.constrs;
if Options.(get_verbose () || get_unsat_core ()) then
Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
if Options.(get_verbose () || get_unsat_core ())
&& not @@ Ex.is_empty d.ex then
Fmt.(box @@ parens @@ pair ~sep:comma pp_constrs Ex.print)
ppf (d.constrs, d.ex)
else
pp_constrs ppf d.constrs

let intersect ~ex d1 d2 =
let constrs = TSet.inter d1.constrs d2.constrs in
Expand Down Expand Up @@ -159,10 +167,10 @@ module Domains = struct
type _ Uf.id += Id : t Uf.id

let pp ppf t =
Fmt.(iter_bindings ~sep:semi MX.iter
(box @@ pair ~sep:(any " ->@ ") X.print Domain.pp)
|> braces
)
Fmt.(box
@@ braces
@@ iter_bindings ~sep:semi MX.iter
@@ pair ~sep:(any " ->@ ") X.print Domain.pp)
ppf t.domains

let empty = { domains = MX.empty; enums = SX.empty; changed = SX.empty }
Expand Down
133 changes: 64 additions & 69 deletions src/lib/reasoners/matching.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ module E = Expr
module ME = E.Map
module SubstE = Var.Map

module MT = Matching_types

let src = Logs.Src.create ~doc:"Matching" __MODULE__
module Log = (val Logs.src_log src : Logs.LOG)

Expand Down Expand Up @@ -94,91 +96,82 @@ module Make (X : Arg) : S with type theory = X.t = struct
(*BISECT-IGNORE-BEGIN*)
module Debug = struct
open Printer
let add_term t =
if Options.get_debug_matching() >= 3 then
print_dbg
~module_name:"Matching" ~function_name:"add_term"
"add_term: %a" E.print t

let matching tr =
if Options.get_debug_matching() >= 3 then
(* let matching tr =
if Options.get_debug_matching() >= 1 then
print_dbg
~module_name:"Matching" ~function_name:"matching"
"@[<v 0>(multi-)trigger: %a@ \
========================================================@]"
E.print_list tr.E.content
E.pp_debug_list tr.E.content *)

let pp_pat ppf Matching_types.{ trigger; _ } =
Expr.print_triggers ppf [trigger]

let matching env =
Log.debug (fun k ->
k "start matching round with known terms:@ %a@ and patterns:@ %a"
Fmt.(box @@ braces
@@ iter_bindings ~sep:comma ME.iter
@@ pair E.pp_debug nop) env.info
Fmt.(box @@ braces
@@ list ~sep:comma pp_pat) env.pats)

let match_pats_modulo pat lsubsts =
if Options.get_debug_matching() >= 3 then
let print fmt Matching_types.{ sbs; sty; _ } =
Format.fprintf fmt ">>> sbs= %a | sty= %a@ "
(SubstE.pp E.print) sbs Ty.print_subst sty
(SubstE.pp E.pp_debug) sbs Ty.print_subst sty
in
print_dbg
~module_name:"Matching" ~function_name:"match_pats_modulo"
"@[<v 2>match_pat_modulo: %a with accumulated substs@ %a@]"
E.print pat (pp_list_no_space print) lsubsts
E.pp_debug pat (pp_list_no_space print) lsubsts

let match_one_pat Matching_types.{ sbs; sty; _ } pat0 =
if Options.get_debug_matching() >= 3 then
if Options.get_debug_matching() >= 1 then
print_dbg
~module_name:"Matching" ~function_name:"match_one_pat"
"match_pat: %a with subst: sbs= %a | sty= %a"
E.print pat0 (SubstE.pp E.print) sbs Ty.print_subst sty
E.pp_debug pat0 (SubstE.pp E.pp_debug) sbs Ty.print_subst sty


let match_one_pat_against Matching_types.{ sbs; sty; _ } pat0 t =
if Options.get_debug_matching() >= 3 then
if Options.get_debug_matching() >= 1 then
print_dbg
~module_name:"Matching" ~function_name:"match_one_pat_against"
"@[<v 0>match_pat: %a against term %a@ \
with subst: sbs= %a | sty= %a@]"
E.print pat0
E.print t
(SubstE.pp E.print) sbs
E.pp_debug pat0
E.pp_debug t
(SubstE.pp E.pp_debug) sbs
Ty.print_subst sty

let match_term Matching_types.{ sbs; sty; _ } t pat =
if Options.get_debug_matching() >= 3 then
print_dbg
~module_name:"Matching" ~function_name:"match_term"
"I match %a against %a with subst: sbs=%a | sty= %a"
E.print pat E.print t (SubstE.pp E.print) sbs Ty.print_subst sty

let match_list Matching_types.{ sbs; sty; _ } pats xs =
if Options.get_debug_matching() >= 3 then
if Options.get_debug_matching() >= 1 then
print_dbg
~module_name:"Matching" ~function_name:"match_list"
"I match %a against %a with subst: sbs=%a | sty= %a"
E.print_list pats
E.print_list xs
(SubstE.pp E.print) sbs
Fmt.(list ~sep:comma E.pp_debug) pats
Fmt.(list ~sep:comma E.pp_debug) xs
(SubstE.pp E.pp_debug) sbs
Ty.print_subst sty

let match_class_of t cl =
if Options.get_debug_matching() >= 3 then
print_dbg
~module_name:"Matching" ~function_name:"match_class_of"
"class_of (%a) = { %a }"
E.print t
(fun fmt -> E.Set.iter (Format.fprintf fmt "%a , " E.print)) cl
Log.debug (fun k -> k
"class_of (%a) = %a"
E.pp_debug t
Fmt.(box @@ braces @@ list ~sep:comma E.pp_debug) cl)

let candidate_substitutions pat_info res =
let open Matching_types in
if Options.get_debug_matching () >= 1 then
print_dbg
~module_name:"Matching" ~function_name:"candidate_substitutions"
"@[<v 2>%3d candidate substitutions for Axiom %a with trigger %a@ "
(List.length res)
E.print pat_info.trigger_orig
E.print_list pat_info.trigger.E.content;
if Options.get_debug_matching() >= 2 then
List.iter
(fun gsbt ->
print_dbg ~header:false
">>> sbs = %a and sbty = %a@ "
(SubstE.pp E.print) gsbt.sbs Ty.print_subst gsbt.sty
)res
if not @@ Compat.List.is_empty res then
Log.debug
(fun k -> k
"found %d candidate substitutions for the axiom %a with \
the multi-trigger:@ %a"
(List.length res)
E.pp_debug pat_info.MT.trigger_orig
Fmt.(box @@ braces @@ list ~sep:comma E.pp_debug)
pat_info.trigger.E.content);

end
(*BISECT-IGNORE-END*)
Expand All @@ -191,7 +184,7 @@ module Make (X : Arg) : S with type theory = X.t = struct

let add_term info t env =
let open Matching_types in
Debug.add_term t;
Log.debug (fun k -> k"add term: %a" E.pp_debug t);
let rec add_rec env t =
if ME.mem t env.info then env
else
Expand Down Expand Up @@ -377,7 +370,15 @@ module Make (X : Arg) : S with type theory = X.t = struct
({ sty = s_ty; gen = g; goal = b; _ } as sg : Matching_types.gsubst)
pat t =
Options.exec_thread_yield ();
Debug.match_term sg t pat;
Log.debug
(fun k ->
k "@[match term@ '%a' against pattern@,'%a' with \
substitution@ (%a, %a)"
E.pp_debug t
E.pp_debug pat
(SubstE.pp E.pp_debug)
sg.sbs
Ty.print_subst sg.sty);
let { E.f = f_pat; xs = pats; ty = ty_pat; _ } = E.term_view pat in
match f_pat with
| Symbols.Var v when Var.equal v Var.underscore ->
Expand Down Expand Up @@ -407,7 +408,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
let cl = if mconf.Util.no_ematching then E.Set.singleton t
else X.class_of tbox t
in
Debug.match_class_of t cl;
let cl =
E.Set.fold
(fun t l ->
Expand Down Expand Up @@ -435,7 +435,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
with Ty.TypeClash _ -> raise Echec

and match_list mconf env tbox sg pats xs =
Debug.match_list sg pats xs;
try
List.fold_left2
(fun sb_l pat arg ->
Expand All @@ -450,8 +449,7 @@ module Make (X : Arg) : S with type theory = X.t = struct

let match_one_pat mconf env tbox pat0 lsbt_acc sg =
Steps.incr (Steps.Matching);
Debug.match_one_pat sg pat0;
let pat = E.apply_subst (sg.sbs, sg.sty) pat0 in
let pat = E.apply_subst (sg.MT.sbs, sg.sty) pat0 in
let { E.f = f; xs = pats; ty = ty; _ } = E.term_view pat in
match f with
| Symbols.Var v -> all_terms v ty env tbox sg lsbt_acc
Expand All @@ -463,7 +461,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
if too_big then lsbt
else
try
Debug.match_one_pat_against sg pat0 t;
let s_ty = Ty.matching sty ty (E.type_info t) in
let gen, but = infos max (||) t g b env in
let sg =
Expand All @@ -479,14 +476,13 @@ module Make (X : Arg) : S with type theory = X.t = struct
with Not_found -> lsbt_acc

let match_pats_modulo mconf env tbox lsubsts pat =
Debug.match_pats_modulo pat lsubsts;
List.fold_left (match_one_pat mconf env tbox pat) [] lsubsts

let matching mconf env tbox pat_info =
let open Matching_types in
let pats = pat_info.trigger in
let pats_list = pats.E.content in
Debug.matching pats;
Debug.matching env;
if List.length pats_list > Options.get_max_multi_triggers_size () then
pat_info, []
else
Expand All @@ -504,7 +500,6 @@ module Make (X : Arg) : S with type theory = X.t = struct
| [_] ->
let res =
List.fold_left (match_pats_modulo mconf env tbox) [egs] pats_list in
Debug.candidate_substitutions pat_info res;
pat_info, res
| _ ->
let cpt = ref 1 in
Expand All @@ -526,7 +521,7 @@ module Make (X : Arg) : S with type theory = X.t = struct
Printer.print_dbg
~module_name:"Matching" ~function_name:"matching"
"skip matching for %a : cpt = %d"
E.print pat_info.trigger_orig !cpt;
E.pp_debug pat_info.trigger_orig !cpt;
pat_info, []

let reset_cache_refs () =
Expand Down Expand Up @@ -657,17 +652,17 @@ module Make (X : Arg) : S with type theory = X.t = struct
(fun lem (guard, age, dep) env ->
match E.form_view lem with
| E.Lemma ({ E.main = f; name; _ } as q) ->
let tgs, kind =
let tgs =
match mconf.Util.backward with
| Util.Normal -> triggers_of q mconf, "Normal"
| Util.Backward -> backward_triggers q, "Backward"
| Util.Forward -> forward_triggers q, "Forward"
| Util.Normal -> triggers_of q mconf
| Util.Backward -> backward_triggers q
| Util.Forward -> forward_triggers q
in
if Options.get_debug_triggers () then
Printer.print_dbg
~module_name:"Matching" ~function_name:"add_triggers"
"@[<v 2>%s triggers of %s are:@ %a@]"
kind name E.print_triggers tgs;
Log.debug (fun k ->
k "add %a triggers of the axiom %s:@ %a"
Util.pp_inst_kind mconf.Util.backward
name
E.print_triggers tgs);
List.fold_left
(fun env tr ->
let info =
Expand Down
Loading

0 comments on commit 83f5ca9

Please sign in to comment.