Bool.SMT
module Log : sig ... end
type sym = Smtml.Symbol.t
type exp = Smtml.Expr.t
val logic : Smtml.Logic.t
val eval : Smtml.Model.t -> Smtml.Symbol.t -> bool
val exp_of_t : bool -> Smtml.Expr.t
val exp_of_s : Smtml.Symbol.t -> Smtml.Expr.t
val add : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t
val mul : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t
val eq : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t
val ge : Smtml.Expr.t -> Smtml.Expr.t -> Smtml.Expr.t
ge a b encodes a ≥ b in the Boolean order (false < true): a ≥ b ↔ (a = b) ∨ (a = true ∧ b = false).
ge a b
a ≥ b
a ≥ b ↔ (a = b) ∨ (a = true ∧ b = false)
val mk : string -> Smtml.Symbol.t * 'a list
Allocate a fresh Boolean SMT symbol. No domain constraints are needed since Ty_bool already restricts the variable to {true, false}.
Ty_bool