Translators (goblint.Goblint_constraint.Translators)

module EqConstrSysFromGlobConstrSys
  (S : ConstrSys.GlobConstrSys) : 
  ConstrSys.EqConstrSys
    with type v = ConstrSys.Var2(S.LVar)(S.GVar).t
     and type d = Lattice.Lift2(S.G)(S.D).t
     and module Var = ConstrSys.Var2(S.LVar)(S.GVar)
     and module Dom = Lattice.Lift2(S.G)(S.D)

Translate a GlobConstrSys into a EqConstrSys

module GlobConstrSolFromEqConstrSolBase
  (S : ConstrSys.GlobConstrSys)
  (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.GlobConstrSys)
  (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.GenericEqIncrSolverBase)
  (S : ConstrSys.GlobConstrSys)
  (LH : Batteries.Hashtbl.S with type key = S.LVar.t)
  (GH : Batteries.Hashtbl.S with type key = S.GVar.t) : 
  sig ... end

Transforms a GenericEqIncrSolver into a GenericGlobIncrSolver.