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. | BitMult of Stdlib.Int.t
  18. | BitCheck
  19. | BitNot
  20. | BitAnd of Stdlib.Int.t
  21. | BitOr of Stdlib.Int.t
  22. | BitXor of Stdlib.Int.t
  23. | BitUnsignedLesser
  24. | BitUnsignedLesserEqual
  25. | BitImplies
  26. | BitShiftLeft
  27. | BitShiftRight
  28. | BitExtraction of Stdlib.Int.t * Stdlib.Int.t
  29. | BitExtensionZero of Stdlib.Int.t
  30. | BitExtensionSign of Stdlib.Int.t
  31. | Membership
  32. | Subset
  33. | Disjoint
  34. | Union of Sort.t
  35. | Inter of Sort.t
  36. | Diff
  37. | Compl
  38. | Enum of Sort.t
  39. | Universe of Sort.t
  40. | ConstArray of Sort.t
  41. | Select
  42. | Store
  43. | Cast of Sort.t
  44. | Constructor of MemoryModel.StructDef.t
  45. | Emp
  46. | Pure
  47. | PointsTo
  48. | Predicate of Identifier.t * MemoryModel.StructDef.t Stdlib.List.t
  49. | HeapTerm of MemoryModel0.Field.t
  50. | BlockBegin
  51. | BlockEnd
  52. | GuardedNot
  53. | Star
  54. | 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