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 DemandEqSolver =
  functor (S : ConstrSys.DemandEqConstrSys) ->
  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). These solver can handle DemandEqConstrSys

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 DemandEqIncrSolverBase =
  functor (S : ConstrSys.DemandEqConstrSys) ->
  functor (H : Batteries.Hashtbl.S with type key = S.v) ->
  sig ... end

module type DemandEqIncrSolver =
  functor (Arg : IncrSolverArg) ->
  DemandEqIncrSolverBase

module type DemandGlobIncrSolver =
  functor (S : ConstrSys.DemandGlobConstrSys) ->
  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)