SolverTypes (goblint.Goblint_constraint.SolverTypes)

module type GenericEqSolver =
  functor (S : ConstrSys.EqConstrSys) ->
  functor (H : Batteries.Hashtbl.S with type key = S.v) ->
  sig ... end

A solver is something that can translate a system into a solution (hash-table)

module type GenericEqIncrSolverBase =
  functor (S : ConstrSys.EqConstrSys) ->
  functor (H : Batteries.Hashtbl.S with type key = S.v) ->
  sig ... end

A solver is something that can translate a system into a solution (hash-table). Incremental solver has data to be marshaled.

module type IncrSolverArg = sig ... end

(Incremental) solver argument, indicating which postsolving should be performed by the solver.

module type GenericEqIncrSolver =
  functor (Arg : IncrSolverArg) ->
  GenericEqIncrSolverBase

An incremental solver takes the argument about postsolving.

module type GenericGlobIncrSolver =
  functor (S : ConstrSys.GlobConstrSys) ->
  functor (LH : Batteries.Hashtbl.S with type key = S.LVar.t) ->
  functor (GH : Batteries.Hashtbl.S with type key = S.GVar.t) ->
  sig ... end

A solver is something that can translate a system into a solution (hash-table)