package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Goblint_constraint.SolverTypesSource

Solver signatures

Sourcemodule type GenericEqSolver = functor (S : ConstrSys.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)

Sourcemodule type DemandEqSolver = functor (S : ConstrSys.DemandEqConstrSys) -> 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). These solver can handle DemandEqConstrSys

Sourcemodule type GenericEqIncrSolverBase = functor (S : ConstrSys.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.

Sourcemodule type IncrSolverArg = sig ... end

(Incremental) solver argument, indicating which postsolving should be performed by the solver.

An incremental solver takes the argument about postsolving.

Sourcemodule type DemandEqIncrSolverBase = functor (S : ConstrSys.DemandEqConstrSys) -> functor (H : Batteries.Hashtbl.S with type key = S.v) -> sig ... end
Sourcemodule type DemandGlobIncrSolver = functor (S : ConstrSys.DemandGlobConstrSys) -> 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)