Module Pulselib.PulseFormulaTableau

module F = Stdlib.Format
module L = IBase.Logging
module CItv = PulseCItv
module SatUnsat = PulseSatUnsat
module Debug = PulseFormulaDebug
module Var = PulseFormulaVar
module Q = QSafeCapped
module LinArith = PulseFormulaLinArit

An implementation of [2] "Solving Linear Arithmetic Constraints" by Harald Rueß and Natarajan Shankar, SRI International, CSL Technical Report CSL-SRI-04-01, 15 January 2004. It uses a Simplex-like technique to reason about inequalities over linear arithmetic expressions.

val pp_var_map : ?filter:((Var.Map.key * 'a) -> bool) -> arrow:string -> (F.formatter -> 'a -> unit) -> (F.formatter -> Var.Map.key -> unit) -> IStdlib.Pp.F.formatter -> 'a Var.Map.t -> unit

As for linear equalities linear_eqs below, the tableau is represented as a map of bindings u -> l meaning u = l.

Invariants:

  • all variables in the tableau are restricted
  • the tableau is feasible: each equality u = c + q1·v1 + ... + qN·vN is such that c>0
val compare : t -> t -> int
val equal : t -> t -> bool
val pp : (F.formatter -> Var.Map.key -> unit) -> IStdlib.Pp.F.formatter -> LinArith.t Var.Map.t -> unit
val yojson_of_t : LinArith.t Var.Map.t -> Yojson.Safe.t
val empty : 'a Var.Map.t
val pivot_unbounded_with_positive_coeff : LinArith.t Var.Map.t -> LinArith.Var.t -> LinArith.t -> LinArith.t Var.Map.t option
val find_pivotable_to : Var.t -> LinArith.t Var.Map.t -> (Var.Map.key * (Var.t * Q.t)) option
val find_pivot : LinArith.t -> LinArith.t Var.Map.t -> (Var.Map.key * (Var.t * Q.t)) option