Module Goblint_constraint.Translators

module EqConstrSysFromDemandConstrSys (S : ConstrSys.DemandEqConstrSys) : ConstrSys.EqConstrSys with type v = S.v and type d = S.d and module Var = S.Var and module Dom = S.Dom

Translate a DemandConstrSys into a EqConstrSys

Translate a DemandGlobConstrSys into a DemandEqConstrSys

module GlobConstrSolFromEqConstrSolBase (S : ConstrSys.DemandGlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) (VH : Batteries.Hashtbl.S with type key = Goblint_constraint__.ConstrSys.Var2(S.LVar)(S.GVar).t) : sig ... end

Splits a EqConstrSys solution into a GlobConstrSys solution with given Hashtbl.S for the EqConstrSys.

module GlobConstrSolFromEqConstrSol (S : ConstrSys.DemandGlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : sig ... end

Splits a EqConstrSys solution into a GlobConstrSys solution.

module GlobSolverFromEqSolver (Sol : SolverTypes.DemandEqIncrSolverBase) (S : ConstrSys.DemandGlobConstrSys) (LH : Batteries.Hashtbl.S with type key = S.LVar.t) (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : sig ... end

Transforms a DemandEqIncrSolver into a DemandGlobIncrSolver.