Skip to content

Clear TD3 sides when not reusing wpoint incrementally #1010

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Mar 22, 2023
Merged

Clear TD3 sides when not reusing wpoint incrementally #1010

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9eb5642
Add wpoint add tracing
sim642 Mar 6, 2023
5ead26a
Add sides to TD3 data statistics
sim642 Mar 6, 2023
c92cc0b
Clear TD3 sides when not reusing wpoint incrementally
sim642 Mar 6, 2023
ad8fa27
Deduplicate TD3 data statistics printing
sim642 Mar 6, 2023
9f53cf1
Refactor TD3 data statistics printing
sim642 Mar 6, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 32 additions & 13 deletions src/solvers/td3.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,11 +74,23 @@ module Base =
dep = HM.create 10;
}

let print_data data str =
let print_data data =
Printf.printf "|rho|=%d\n" (HM.length data.rho);
Printf.printf "|stable|=%d\n" (HM.length data.stable);
Printf.printf "|infl|=%d\n" (HM.length data.infl);
Printf.printf "|wpoint|=%d\n" (HM.length data.wpoint);
Printf.printf "|sides|=%d\n" (HM.length data.sides);
Printf.printf "|side_dep|=%d\n" (HM.length data.side_dep);
Printf.printf "|side_infl|=%d\n" (HM.length data.side_infl);
Printf.printf "|var_messages|=%d\n" (HM.length data.var_messages);
Printf.printf "|rho_write|=%d\n" (HM.length data.rho_write);
Printf.printf "|dep|=%d\n" (HM.length data.dep);
Hooks.print_data ()

let print_data_verbose data str =
if GobConfig.get_bool "dbg.verbose" then (
Printf.printf "%s:\n|rho|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n"
str (HM.length data.rho) (HM.length data.stable) (HM.length data.infl) (HM.length data.wpoint) (HM.length data.side_dep) (HM.length data.side_infl) (HM.length data.var_messages) (HM.length data.rho_write) (HM.length data.dep);
Hooks.print_data ()
Printf.printf "%s:\n" str;
print_data data
)

let verify_data data =
Expand Down Expand Up @@ -197,8 +209,10 @@ module Base =
HM.clear data.stable;
HM.clear data.infl
);
if not reuse_wpoint then
if not reuse_wpoint then (
HM.clear data.wpoint;
HM.clear data.sides
Copy link
Member Author

@sim642 sim642 Mar 6, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The real change is just this line being added.

);
data
| None ->
create_empty_data ()
Expand Down Expand Up @@ -241,14 +255,13 @@ module Base =
let dep = data.dep in

let () = print_solver_stats := fun () ->
Printf.printf "|rho|=%d\n|called|=%d\n|stable|=%d\n|infl|=%d\n|wpoint|=%d\n|side_dep|=%d\n|side_infl|=%d\n|var_messages|=%d\n|rho_write|=%d\n|dep|=%d\n"
(HM.length rho) (HM.length called) (HM.length stable) (HM.length infl) (HM.length wpoint) (HM.length side_dep) (HM.length side_infl) (HM.length var_messages) (HM.length rho_write) (HM.length dep);
Hooks.print_data ();
print_data data;
Printf.printf "|called|=%d\n" (HM.length called);
print_context_stats rho
in

if GobConfig.get_bool "incremental.load" then (
print_data data "Loaded data for incremental analysis";
print_data_verbose data "Loaded data for incremental analysis";
verify_data data
);

Expand Down Expand Up @@ -379,6 +392,7 @@ module Base =
HM.replace restarted_wpoint y ();
)
);
if tracing then trace "sol2" "eval adding wpoint %a from %a\n" S.Var.pretty_trace y S.Var.pretty_trace x;
HM.replace wpoint y ();
);
let tmp = simple_solve l x y in
Expand Down Expand Up @@ -426,7 +440,12 @@ module Base =
HM.replace rho y tmp;
if side_widen <> "cycle" then destabilize y;
(* make y a widening point if ... This will only matter for the next side _ y. *)
let wpoint_if e = if e then HM.replace wpoint y () in
let wpoint_if e =
if e then (
if tracing then trace "sol2" "side adding wpoint %a from %a\n" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x;
HM.replace wpoint y ()
)
in
match side_widen with
| "always" -> (* Any side-effect after the first one will be widened which will unnecessarily lose precision. *)
wpoint_if true
Expand Down Expand Up @@ -726,7 +745,7 @@ module Base =
delete_marked rho_write;
HM.iter (fun x w -> delete_marked w) rho_write;

print_data data "Data after clean-up";
print_data_verbose data "Data after clean-up";

(* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *)

Expand Down Expand Up @@ -828,7 +847,7 @@ module Base =
);

stop_event ();
print_data data "Data after solve completed";
print_data_verbose data "Data after solve completed";

if GobConfig.get_bool "dbg.print_wpoints" then (
Printf.printf "\nWidening points:\n";
Expand Down Expand Up @@ -1016,7 +1035,7 @@ module Base =
let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in
Post.post st (stable_reluctant_vs @ vs) rho;

print_data data "Data after postsolve";
print_data_verbose data "Data after postsolve";

verify_data data;
(rho, {st; infl; sides; rho; wpoint; stable; side_dep; side_infl; var_messages; rho_write; dep})
Expand Down