Module Pulselib.PulseCItv

module F = Stdlib.Format
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val equal_to : IR.IntLit.t -> t
val is_equal_to_zero : t -> bool
val is_not_equal_to_zero : t -> bool

whether this is literally ≠0

val pp : F.formatter -> t -> unit
type abduction_result =
| Unsatisfiable

the assertion is never true given the parameters

| Satisfiable of t option * t option

the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals

val abduce_binop_is_true : negated:bool -> IR.Binop.t -> t option -> t option -> abduction_result

given arith_lhs_opt bop arith_rhs_opt and if not negated, return either

  • Unsatisfiable iff lhs bop rhs = ∅
  • Satisfiable (abduced_lhs_opt,abduced_rhs_opt) iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is None, same for rhs) abduced_lhs_opt=Some alhs if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)

If negated then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.

val binop : IR.Binop.t -> t -> t -> t option
val unop : IR.Unop.t -> t -> t option
val zero_inf : t
val ge_to : IR.IntLit.t -> t