Module Bottleneck.SMT

module Log : sig ... end
type sym = Smtml.Symbol.t
type exp = Smtml.Expr.t
val logic : Smtml.Logic.t
val neg_inf_v : int
val pos_inf_v : int
val eval : Smtml.Model.t -> Smtml.Symbol.t -> t
val exp_of_t : t -> Smtml.Expr.t
val exp_of_s : Smtml.Symbol.t -> Smtml.Expr.t
val is_neg_inf : Smtml.Expr.t -> Smtml.Expr.t
val is_pos_inf : Smtml.Expr.t -> Smtml.Expr.t
val int_min : Smtml.Expr.t -> Smtml.Expr.t -> Smtml__Expr.t
val int_max : Smtml.Expr.t -> Smtml.Expr.t -> Smtml__Expr.t
val add : Smtml.Expr.t -> Smtml.Expr.t -> Smtml__Expr.t

SMT-level max, guarding the PosInf sentinel first (PosInf absorbs).

val mul : Smtml.Expr.t -> Smtml.Expr.t -> Smtml__Expr.t

SMT-level min, guarding the NegInf sentinel first (NegInf absorbs).

val eq : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t
val ge : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t

ge e1 e2: e1 ≥ e2 in the bottleneck order; PosInf ≥ everything, everything ≥ NegInf.

val mk : string -> Smtml.Symbol.t * Smtml.Expr.t list

Domain constraint: sym ≥ -2 keeps the variable within the sentinel-encoded carrier {-2, -1} ∪ 0, +∞).