docs menu

Module Shape.Sint

Symbolic integers.

Arithmetic computes on integers, and builds nodes as soon as an operand is symbolic. It is exact: a result that does not fit an int raises Invalid_argument.

#type node := Ops.t

#type t = Ops.sint

#val (+) : t -> t -> t

#val (-) : t -> t -> t

#val (*) : t -> t -> t

#val (//) : t -> t -> t

Division rounding towards negative infinity.

#val (%) : t -> t -> t

The remainder of //, with the sign of the divisor.

#val prod : t list -> t

prod ss is the product of ss, Int 1 if empty.

#type cond =

#| Known of bool
#| Cond of node

The type for conditions on symbolic integers: known, or a boolean node.

#val (<) : t -> t -> cond

#val (<=) : t -> t -> cond

#val (>) : t -> t -> cond

#val (>=) : t -> t -> cond

#val (<>) : t -> t -> cond

#val resolve : ?default:bool -> cond -> bool

resolve ~default c is c's value if known, and Shape.resolve's otherwise.

#val truth : cond -> bool

truth c is c's value if known, and Shape.to_bool's otherwise.

#val equal : t -> t -> bool

equal s0 s1 is true iff both are the same integer or the same node. It does not decide whether two nodes have the same value.

#val pp : Stdlib.Format.formatter -> t -> unit

pp formats an integer in decimal, and a node as Ops.pp does.