Translators (goblint.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

module EqConstrSysFromGlobConstrSys
  (S : ConstrSys.DemandGlobConstrSys) : 
  ConstrSys.DemandEqConstrSys
    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 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 DemandEqIncrSolverFromGenericEqIncrSolver
  (Sol : SolverTypes.GenericEqIncrSolver) : 
  SolverTypes.DemandEqIncrSolver

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.