Goblint_solver.Td3Incremental/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 = Messagesmodule type Hooks = sig ... endmodule Base
(Arg : ConstrSys.IncrSolverArg)
(S : ConstrSys.EqConstrSys)
(HM : Batteries.Hashtbl.S with type key = S.v)
(Hooks : Hooks with module S = S and module HM = HM)
(UpdateRule : Td3UpdateRule.S) :
sig ... endmodule Basic (UpdateRule : Td3UpdateRule.S) : ConstrSys.GenericEqIncrSolverTD3 with no hooks.
module DepVals (UpdateRule : Td3UpdateRule.S) : ConstrSys.GenericEqIncrSolverTD3 with eval skipping using dep_vals.