Module `Bitfields.IntBitfields`Source

Bitfields - Sequences of bits that can be set, cleared, or unknown

We rely on Zarith for arithmetic operations.

Types

Sourcetype t = Z.t * Z.t

cleared

Sourcetype t_with_bot = t Utils_core.Bot.with_bot

The type of possibly empty bitfields.

module I = ItvUtils.IntItv

module B = ItvUtils.IntBound

module C = CongUtils.IntCong

Sourceval is_valid : t -> bool

Every bit in a bitfield must be set, cleared, or both.

Constructors

Sourceval of_z : Z.t -> Z.t -> t

Sourceval of_z_bot : Z.t -> Z.t -> t_with_bot

Sourceval cst : Z.t -> t

Constant.

Sourceval cst_int : int -> t

Sourceval cst_int64 : int64 -> t

Sourceval zero : t

Sourceval one : t

Sourceval mone : t

-1

Sourceval zero_one : t

0,1

Sourceval minf_inf : t

All integers. Indistiguishable from 0,+∞.

Sourceval unsigned : int -> t

Bitfields of unsigned integers with the specified bitsize.

Sourceval unsigned8 : t

Sourceval unsigned16 : t

Sourceval unsigned32 : t

Sourceval unsigned64 : t

Sourceval of_range_bot : Z.t -> Z.t -> t Utils_core.Bot.with_bot

Bitfield enclosing the range lo,hi.

Sourceval of_bound_bot : B.t -> B.t -> t Utils_core.Bot.with_bot

Bitfield enclosing the range lo,hi.

Sourceval of_range : Z.t -> Z.t -> t

Bitfield enclosing the range lo,hi. Fails with invalid_arg if the range is empty.

Sourceval of_bound : B.t -> B.t -> t

Bitfield enclosing the range lo,hi. Fails with invalid_arg if the range is empty.

Predicates

Sourceval equal : t -> t -> bool

Equality. = also works.

Sourceval equal_bot : t_with_bot -> t_with_bot -> bool

Sourceval included : t -> t -> bool

Set ordering.

Sourceval included_bot : t_with_bot -> t_with_bot -> bool

Sourceval intersect : t -> t -> bool

Whether the intersection is non-empty.

Sourceval intersect_bot : t_with_bot -> t_with_bot -> bool

Sourceval contains : Z.t -> t -> bool

Sourceval compare : t -> t -> int

A total ordering on bitfields, returning -1, 0, or 1. Can be used as compare for sets, maps, etc.

Sourceval compare_bot : t Utils_core.Bot.with_bot -> t Utils_core.Bot.with_bot -> int

Total ordering on possibly empty bitfields.

Sourceval contains_zero : t -> bool

Whether the bifield contains zero.

Sourceval contains_one : t -> bool

Whether the bifield contains one.

Sourceval contains_nonzero : t -> bool

Whether the bifield contains a non-zero value.

Sourceval is_zero : t -> bool

Sourceval is_positive : t -> bool

Sourceval is_positive_strict : t -> bool

Sourceval is_negative_strict : t -> bool

Sourceval is_negative : t -> bool

Sourceval is_nonzero : t -> bool

Contains only non-zero elements.

Sourceval is_minf_inf : t -> bool

The bitfield represents -∞,+∞.

Sourceval is_singleton : t -> bool

Whether the bitfield contains a single element.

Sourceval is_bounded : t -> bool

Whether the bitfield contains a finite number of elements.

Sourceval lower_bound : t -> B.t

Get the lower bound (possibly MINF).

Sourceval upper_bound : t -> B.t

Get the upper bound (possibly PINF).

Printing

Sourceval to_string : t -> string

Sourceval print : Stdlib.out_channel -> t -> unit

Sourceval fprint : Stdlib.Format.formatter -> t -> unit

Sourceval bprint : Stdlib.Buffer.t -> t -> unit

Sourceval to_string_bot : t Utils_core.Bot.with_bot -> string

Sourceval print_bot : Stdlib.out_channel -> t Utils_core.Bot.with_bot -> unit

Sourceval fprint_bot : Stdlib.Format.formatter -> t Utils_core.Bot.with_bot -> unit

Sourceval bprint_bot : Stdlib.Buffer.t -> t Utils_core.Bot.with_bot -> unit

Enumeration

Sourceval size : t -> int

Number of elements. Raises an invalid argument if it is unbounded.

Sourceval to_list : t -> Z.t list

List of elements, in increasing order. Raises an invalid argument if it is unbounded.

Set operations

Sourceval join : t -> t -> t

Abstract union.

Sourceval join_bot : t_with_bot -> t_with_bot -> t_with_bot

Sourceval join_list : t list -> t_with_bot

Sourceval meet : t -> t -> t_with_bot

Abstract intersection.

Sourceval meet_bot : t_with_bot -> t_with_bot -> t_with_bot

Sourceval meet_list : t list -> t_with_bot

Forward operations

Sourceval to_bool : bool -> bool -> t

Sourceval log_cast : t -> t

Conversion from integer to boolean in 0,1: maps 0 to 0 (false) and non-zero to 1 (true).

Sourceval log_not : t -> t

Logical negation. Logical operation use the C semantics: they accept 0 and non-0 respectively as false and true, but they always return 0 and 1 respectively for false and true.

Sourceval log_and : t -> t -> t

Logical and.

Sourceval log_or : t -> t -> t

Logical or.

Sourceval log_xor : t -> t -> t

Logical exclusive or.

Sourceval log_eq : t -> t -> t

Sourceval log_neq : t -> t -> t

Sourceval log_leq : t -> t -> t

Sourceval log_geq : t -> t -> t

Sourceval log_lt : t -> t -> t

Sourceval log_gt : t -> t -> t

C comparison tests. Returns an interval included in 0,1 (a boolean)

Sourceval is_log_eq : t -> t -> bool

Sourceval is_log_neq : t -> t -> bool

Sourceval is_log_leq : t -> t -> bool

Sourceval is_log_geq : t -> t -> bool

Sourceval is_log_lt : t -> t -> bool

Sourceval is_log_gt : t -> t -> bool

C comparison tests. Returns a boolean if the test may succeed

Sourceval shift_left : t -> t -> t

Bitshift left: multiplication by a power of 2.

Sourceval shift_right : t -> t -> t

Bitshift right: division by a power of 2 rounding towards -∞.

Sourceval shift_right_trunc : t -> t -> t

Unsigned bitshift right: division by a power of 2 with truncation.

Sourceval bit_not : t -> t

Bitwise negation.

Sourceval bit_or : t -> t -> t

Bitwise or.

Sourceval bit_and : t -> t -> t

Bitwise and.

Sourceval bit_xor : t -> t -> t

Bitwise exclusive or.

Filters

Given two interval aruments, return the arguments assuming that the predicate holds.

Sourceval filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot

Source

val filter_sgl : 
  (Z.t -> Z.t -> bool) ->
  t ->
  t ->
  (t * t) Utils_core.Bot.with_bot

Sourceval filter_neq : t -> t -> (t * t) Utils_core.Bot.with_bot

Sourceval filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot

Sourceval filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot

Sourceval filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot

Sourceval filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot

Reduction

Sourceval of_interval : I.t -> t

Sourceval to_interval : t -> I.t

Sourceval meet_inter : t -> I.t -> (t * I.t) Utils_core.Bot.with_bot

Intersects a bitfield with an interval, and returns the set represented both as a bitfield and as an interval. Useful to implement reductions.

Install

Dune Dependency

Authors

Maintainers

Sources

doc/bitfields/Bitfields/IntBitfields/index.html

Module `Bitfields.IntBitfields`Source

Types

Constructors

Predicates

Printing

Enumeration

Set operations

Forward operations

Filters

Reduction

package mopsa

Install

Dune Dependency

Authors

Maintainers

Sources

doc/bitfields/Bitfields/IntBitfields/index.html

Module Bitfields.IntBitfieldsSource

Types

Constructors

Predicates

Printing

Enumeration

Set operations

Forward operations

Filters

Reduction

Module `Bitfields.IntBitfields`Source