Goblint_solver.Td3
Incremental/interactive terminating top-down solver, which supports space-efficiency and caching (td3
).
Incremental terminating top down solver that optionally only keeps values at widening points and restores other values afterwards.
module M = Messages
module type Hooks = sig ... end
module Base
(Arg : Goblint_constraint.SolverTypes.IncrSolverArg)
(S : Goblint_constraint.ConstrSys.DemandEqConstrSys)
(HM : Batteries.Hashtbl.S with type key = S.v)
(Hooks : Hooks with module S = S and module HM = HM)
(UpdateRule : Td3UpdateRule.S) :
sig ... end
TD3 with no hooks.
TD3 with eval skipping using dep_vals
.