Introduce a simplified version of td3 with warrowing #1611
Conversation
| (** Terminating op-down solver with side effects. Baseline for comparisons with td_parallel solvers ([td_simplified]).*) | ||
|
|
||
| (** Top down solver that uses the box-operator for widening/narrowing at widening points. | ||
| * Options: | ||
| * - solvers.td3.remove-wpoint (default: true): Remove widening points when a variable is and stays stable in iterate. Increases precision of nested loops.*) |
There was a problem hiding this comment.
I'm not sure how much we want to iterate on this. This solver isn't too important to us, but it's supposed to be didactic, so maybe we should spend time polishing this.
The following thoughts are first for discussion than immediate requests for changes.
Anyway, if it's "terminating" then it cannot be the warrowing version (which is non-terminating). The first improvement of TD3 is the termination by switching from warrowing to widen/narrow phases. Personally, I would prefer the phased version instead of warrowing: it's not really more complicated (just one argument to solve).
As to the remove-wpoint improvement, I wouldn't have it in this simplified version because it is niche not necessary for the simple presentation.
| type solver_data = { | ||
| infl: VS.t HM.t; | ||
| rho: S.Dom.t HM.t; | ||
| wpoint: unit HM.t; | ||
| stable: unit HM.t; | ||
| } | ||
|
|
||
| let create_empty_data () = { | ||
| infl = HM.create 10; | ||
| rho = HM.create 10; | ||
| wpoint = HM.create 10; | ||
| stable = HM.create 10; | ||
| } | ||
|
|
||
| let print_data data = | ||
| Logs.debug "|rho|=%d" (HM.length data.rho); | ||
| Logs.debug "|stable|=%d" (HM.length data.stable); | ||
| Logs.debug "|infl|=%d" (HM.length data.infl); | ||
| Logs.debug "|wpoint|=%d" (HM.length data.wpoint) |
There was a problem hiding this comment.
These being in a record was needed for incremental marshaling in TD3, but this isn't incremental, so I'd just have normal variables for these (like in all other solvers).
| let rec iterate ?reuse_eq x = (* ~(inner) solve in td3*) | ||
| let query x y = (* ~eval in td3 *) |
There was a problem hiding this comment.
Is there a reason that query and side are inside iterate/solve here? This makes iterate (which begins a long way down) quite large, which is also apparent from the need to explicitly comment where iterate begins. And the x argument of iterate is always the x argument of query/side, so there's unnecessary duplication.
The simplified warrowing solver as implemented by @FelixKrayer .
Since changes were intervened in many commits with other changes, it would have been too much effort to keep authorship information on git and I have copied the file instead. Maybe Felix can open an issue with the same change.
As to which solver we should keep as the simplified version, this one: