BaseLogic.Boolean
include module type of struct include Boolean0 end
val mk_const : Stdlib.Bool.t -> t
val tt : t
val ff : t
include module type of struct include Equality end
val mk_eq : Self.t Stdlib.List.t -> t
val mk_distinct : t Stdlib.List.t -> t
val mk_eq2 : Self.t -> Self.t -> t
val mk_distinct2 : t -> t -> t
val mk_var : string -> t
val mk_fresh_var : string -> t
val mk_and : Self.t Stdlib.List.t -> Self.t
We can never simplify pure(phi) /\ emp ~> pure(phi) to be able to represent formulae in imprecise semantics.
TODO: is this still true?
val mk_or : Self.t Stdlib.List.t -> Self.t
val mk_not : t -> t
Not valid for separation logic with precise semantics!
val mk_implies : Self.t -> Self.t -> Self.t
val mk_iff : t Stdlib.List.t -> t
val mk_ite : Self.t -> Self.t -> Self.t -> Self.t
val mk_multiple_ite : (Self.t * Self.t) list -> Self.t -> Self.t
val mk_and2 : Self.t -> Self.t -> Self.t
Some syntax sugar
val mk_or2 : Self.t -> Self.t -> Self.t