Translators (p.goblint.2.6.0.doc.goblint.constraint.Goblint

Source

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

Source

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

Source

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 = ConstrSys.Var2(S.LVar)(S.GVar).t) : 
  sig ... end

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

Source

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.

Source

module DemandEqIncrSolverFromGenericEqIncrSolver
  (Sol : SolverTypes.GenericEqIncrSolver) : 
  SolverTypes.DemandEqIncrSolver

Source

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.