Module Prob.SMT

module Log : sig ... end
type sym = Smtml.Symbol.t * Smtml.Symbol.t

A probability symbol is represented as (num, den) integer pair.

type exp = Smtml.Expr.t * Smtml.Expr.t
val logic : Smtml.Logic.t
val exp_of_t : Q.t -> Smtml.Expr.t * Smtml.Expr.t
val exp_of_s : (Smtml.Symbol.t * Smtml.Symbol.t) -> Smtml.Expr.t * Smtml.Expr.t
val eval : Smtml.Model.t -> (Smtml.Symbol.t * Smtml.Symbol.t) -> Q.t
val ge : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t
val eq : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t
val add : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml__Expr.t * Smtml.Expr.t

add (n1/d1) (n2/d2) = min(n1·d2 + n2·d1, d1·d2) / (d1·d2). The ITE implements the truncation at 1 in the symbolic domain.

val mul : (Smtml.Expr.t * Smtml.Expr.t) -> (Smtml.Expr.t * Smtml.Expr.t) -> Smtml.Expr.t * Smtml.Expr.t
val mk : Base.String.t -> (Smtml.Symbol.t * Smtml.Symbol.t) * Smtml.Expr.t list

Domain constraints: den > 0, num ≥ 0, den ≥ num (value in 0,1).