package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

IntCong - Integer congruences.

We rely on Zarith for arithmetic operations.

Types

type t = Z.t * Z.t

offset

type t_with_bot = t Utils_core.Bot.with_bot

The type of possibly empty congruence sets.

val is_valid : t -> bool
module I = ItvUtils.IntItv

Arithmetic utilities

val gcd : Z.t -> Z.t -> Z.t

Greatest common divisor of |a| and |b|. 0 is neutral.

val gcd3 : Z.t -> Z.t -> Z.t -> Z.t
val gcd_ext : Z.t -> Z.t -> Z.t * Z.t * Z.t * Z.t

Returns the gcd, lcm and cofactors u, v such that ua+vb=gcd. Undefined if a or b is 0.

val divides : Z.t -> Z.t -> bool

Wheter b is a multiple of a. Always true if b = 0.

val rem_zero : Z.t -> Z.t -> Z.t

As Z.erem, but rem_zero a 0 = a.

Constructors

val of_z : Z.t -> Z.t -> t

Returns aℤ + b.

val of_int : int -> int -> t
val of_int64 : int64 -> int64 -> t
val cst : Z.t -> t

Returns 0ℤ + b

val cst_int : int -> t
val cst_int64 : int64 -> t
val zero : t

0ℤ+0

val one : t

0ℤ+1

val mone : t

0ℤ-1

val minf_inf : t

1ℤ+0

val of_range : Z.t -> Z.t -> t
val of_range_bot : Z.t -> Z.t -> t Utils_core.Bot.with_bot
val of_bound : B.t -> B.t -> t
val of_bound_bot : B.t -> B.t -> t Utils_core.Bot.with_bot

Congruence overapproximating an interval.

Predicates

val equal : t -> t -> bool

Equality. = also works.

val equal_bot : t_with_bot -> t_with_bot -> bool
val included : t -> t -> bool

Set ordering.

val included_bot : t_with_bot -> t_with_bot -> bool
val intersect : t -> t -> bool

Whether the intersection is non-empty.

val intersect_bot : t_with_bot -> t_with_bot -> bool
val contains : Z.t -> t -> bool

Whether the set contains some value x.

val compare : t -> t -> int

A total ordering (lexical ordering) returning -1, 0, or 1. Can be used as compare for sets, maps, etc.

Total ordering on possibly empty congruences.

val contains_zero : t -> bool

Whether the congruence contains zero.

val contains_one : t -> bool

Whether the congruence contains one.

val contains_nonzero : t -> bool

Whether the congruence contains a non-zero value.

val is_zero : t -> bool
val is_positive : t -> bool
val is_negative : t -> bool
val is_positive_strict : t -> bool
val is_negative_strict : t -> bool
val is_nonzero : t -> bool

Sign.

val is_minf_inf : t -> bool

The congruence represents -∞,+∞.

val is_singleton : t -> bool

Whether the congruence contains a single element.

val is_bounded : t -> bool

Whether the congruence contains a finite number of elements.

val is_in_range : t -> Z.t -> Z.t -> bool

Whether the congruence is included in the range lo,up.

Printing

val to_string : t -> string
val print : Stdlib.out_channel -> t -> unit
val fprint : Stdlib.Format.formatter -> t -> unit
val bprint : Stdlib.Buffer.t -> t -> unit
val to_string_bot : t Utils_core.Bot.with_bot -> string
val print_bot : Stdlib.out_channel -> t Utils_core.Bot.with_bot -> unit
val fprint_bot : Stdlib.Format.formatter -> t Utils_core.Bot.with_bot -> unit
val bprint_bot : Stdlib.Buffer.t -> t Utils_core.Bot.with_bot -> unit

Set operations

val join : t -> t -> t

Abstract union.

val join_bot : t_with_bot -> t_with_bot -> t_with_bot
val join_list : t list -> t_with_bot
val meet : t -> t -> t_with_bot

Abstract intersection.

val meet_bot : t_with_bot -> t_with_bot -> t_with_bot
val meet_list : t list -> t_with_bot
val meet_range : t -> Z.t -> Z.t -> t_with_bot

Abstract intersection with lo,up.

val positive : t -> t_with_bot
val negative : t -> t_with_bot

Positive and negative part.

val meet_zero : t -> t_with_bot

Intersects with

.

val meet_nonzero : t -> t_with_bot

Keeps only non-zero elements.

Forward operations

val neg : t -> t

Negation.

val abs : t -> t

Absolute value.

val succ : t -> t

Adding 1.

val pred : t -> t

Subtracting 1.

val add : t -> t -> t

Addition.

val sub : t -> t -> t

Subtraction.

val mul : t -> t -> t

Multiplication.

val div : t -> t -> t_with_bot

Division (with truncation).

val rem : t -> t -> t_with_bot

Remainder. Uses the C semantics for remainder (%).

val wrap : t -> Z.t -> Z.t -> t

Put back inside lo,up by modular arithmetics.

val to_bool : bool -> bool -> t
val log_cast : t -> t

Conversion from integer to boolean in 0,1: maps 0 to 0 (false) and non-zero to 1 (true). 0;1 is over-approximated as ℤ.

val 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. 0;1 is over-approximated as ℤ.

val log_and : t -> t -> t

Logical and.

val log_or : t -> t -> t

Logical or.

val log_xor : t -> t -> t

Logical exclusive or.

val log_eq : t -> t -> t
val log_neq : t -> t -> t
val log_sgl : (Z.t -> Z.t -> bool) -> t -> t -> t
val log_leq : t -> t -> t
val log_geq : t -> t -> t
val log_lt : t -> t -> t
val log_gt : t -> t -> t

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

val is_log_eq : t -> t -> bool
val is_log_neq : t -> t -> bool
val is_log_sgl : (Z.t -> Z.t -> bool) -> t -> t -> bool
val is_log_leq : t -> t -> bool
val is_log_geq : t -> t -> bool
val is_log_lt : t -> t -> bool
val is_log_gt : t -> t -> bool

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

val shift_left : t -> t -> t_with_bot

Bitshift left: multiplication by a power of 2.

val shift_right : t -> t -> t_with_bot

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

val shift_right_trunc : t -> t -> t_with_bot

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

val bit_not : t -> t

Bitwise negation: ~x = -x-1

Filters

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

val filter_eq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_sgl : (Z.t -> Z.t -> bool) -> t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_neq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_leq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_geq : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_lt : t -> t -> (t * t) Utils_core.Bot.with_bot
val filter_gt : t -> t -> (t * t) Utils_core.Bot.with_bot

Backward operations

Given one or two interval argument(s) and a result interval, return the argument(s) assuming the result in the operation is in the given result.

val bwd_neg : t -> t -> t_with_bot
val bwd_abs : t -> t -> t_with_bot
val bwd_succ : t -> t -> t_with_bot
val bwd_pred : t -> t -> t_with_bot
val bwd_add : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_sub : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_mul : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_bit_not : t -> t -> t_with_bot
val bwd_join : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Backward join: both arguments and intersected with the result.

val bwd_rem : t -> t -> t -> (t * (Z.t * Z.t)) Utils_core.Bot.with_bot
val bwd_div : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_wrap : t -> 'a -> t -> t_with_bot
val bwd_shift_left : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_shift_right : t -> t -> t -> (t * t) Utils_core.Bot.with_bot
val bwd_shift_right_trunc : t -> t -> t -> (t * t) Utils_core.Bot.with_bot

Reduction

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

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct