ConstrSys (goblint.ConstrSys)

module type SysVar = sig ... end

module type VarType = sig ... end

type 'v sys_change_info = {

obsolete : 'v list;
(*
Variables to destabilize.
*)
delete : 'v list;
(*
Variables to delete.
*)
reluctant : 'v list;
(*
Variables to solve reluctantly.
*)
restart : 'v list;
(*
Variables to restart.
*)

}

Abstract incremental change to constraint system.

parameter 'v
constrain system variable type

module type MonSystem = sig ... end

A side-effecting system.

module type EqConstrSys = MonSystem with type 'a m := 'a option

Any system of side-effecting equations over lattices.

module type GlobConstrSys = sig ... end

A side-effecting system with globals.

module type GenericEqIncrSolverBase =
  functor (S : 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 GenericEqSolver =
  functor (S : 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 GenericGlobSolver =
  functor (S : GlobConstrSys) ->
  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)

module Var2
  (LV : VarType)
  (GV : VarType) : 
  VarType with type t = [ `L of LV.t | `G of GV.t ]

Combined variables so that we can also use the more common EqConstrSys that uses only one kind of a variable.

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

Translate a GlobConstrSys into a EqConstrSys

module GlobConstrSolFromEqConstrSolBase
  (S : 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 = 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 : 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 : GenericEqIncrSolverBase)
  (S : 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 GenericGlobSolver.

module CurrentVarEqConstrSys (S : EqConstrSys) : sig ... end

EqConstrSys where current_var indicates the variable whose right-hand side is currently being evaluated.