Module BaseLogic.Application

type t =
  1. | Constant of Constant.t
  2. | Equal
  3. | Distinct
  4. | And
  5. | Or
  6. | Not
  7. | Implies
  8. | Iff
  9. | IfThenElse
  10. | Plus
  11. | Minus
  12. | Mult
  13. | Lesser
  14. | LesserEqual
  15. | BitPlus of Stdlib.Int.t
  16. | BitNeg
  17. | BitCheck
  18. | BitNot
  19. | BitAnd of Stdlib.Int.t
  20. | BitOr of Stdlib.Int.t
  21. | BitXor of Stdlib.Int.t
  22. | BitUnsignedLesser
  23. | BitUnsignedLesserEqual
  24. | BitImplies
  25. | BitShiftLeft
  26. | BitShiftRight
  27. | Membership
  28. | Subset
  29. | Disjoint
  30. | Union of Sort.t
  31. | Inter of Sort.t
  32. | Diff
  33. | Compl
  34. | Enum of Sort.t
  35. | Universe of Sort.t
  36. | ConstArray of Sort.t
  37. | Select
  38. | Store
  39. | Cast of Sort.t
  40. | Constructor of MemoryModel.StructDef.t
  41. | Emp
  42. | Pure
  43. | PointsTo
  44. | Predicate of Identifier.t * MemoryModel.StructDef.t Stdlib.List.t
  45. | HeapTerm of MemoryModel0.Field.t
  46. | BlockBegin
  47. | BlockEnd
  48. | GuardedNot
  49. | Star
  50. | Septraction
val equal : t -> t -> bool
val compare : t -> t -> int
val can_reorder : t -> bool

TODO: So far only used for tests. Proper implementation can be used for comparison.

val show : t -> string
val get_sort : t -> Sort.t list -> Sort.t