Module `CongUtils.IntCong`

IntCong - Integer congruences.

We rely on Zarith for arithmetic operations.

Types

type t = Z.t * Z.t

offset

type t_with_bot = t Core.Bot.with_bot

The type of possibly empty congruence sets.

val is_valid : t -> bool

module I = ItvUtils.IntItv

module B = ItvUtils.IntBound

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 Core.Bot.with_bot

val of_bound : B.t -> B.t -> t

val of_bound_bot : B.t -> B.t -> t 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.

val compare_bot : t Core.Bot.with_bot -> t Core.Bot.with_bot -> int

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 : out_channel -> t -> unit

val fprint : Format.formatter -> t -> unit

val bprint : Buffer.t -> t -> unit

val to_string_bot : t Core.Bot.with_bot -> string

val print_bot : out_channel -> t Core.Bot.with_bot -> unit

val fprint_bot : Format.formatter -> t Core.Bot.with_bot -> unit

val bprint_bot : Buffer.t -> t 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) Core.Bot.with_bot

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

val filter_neq : t -> t -> (t * t) Core.Bot.with_bot

val filter_leq : t -> t -> (t * t) Core.Bot.with_bot

val filter_geq : t -> t -> (t * t) Core.Bot.with_bot

val filter_lt : t -> t -> (t * t) Core.Bot.with_bot

val filter_gt : t -> t -> (t * t) 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) Core.Bot.with_bot

val bwd_sub : t -> t -> t -> (t * t) Core.Bot.with_bot

val bwd_mul : t -> t -> t -> (t * t) Core.Bot.with_bot

val bwd_bit_not : t -> t -> t_with_bot

val bwd_join : t -> t -> t -> (t * t) Core.Bot.with_bot

Backward join: both arguments and intersected with the result.

val bwd_rem : t -> t -> t -> (t * (Z.t * Z.t)) Core.Bot.with_bot

val bwd_div : t -> t -> t -> (t * t) Core.Bot.with_bot

val bwd_wrap : t -> 'a -> t -> t_with_bot

val bwd_shift_left : t -> t -> t -> (t * t) Core.Bot.with_bot

val bwd_shift_right : t -> t -> t -> (t * t) Core.Bot.with_bot

val bwd_shift_right_trunc : t -> t -> t -> (t * t) Core.Bot.with_bot

Reduction

val meet_inter : t -> I.t -> (t * I.t) 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.

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/CongUtils/IntCong/index.html

Module `CongUtils.IntCong`

Types

Arithmetic utilities

Constructors

Predicates

Printing

Set operations

Forward operations

Filters

Backward operations

Reduction

package mopsa

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/mopsa.mopsa_utils/Mopsa_utils/CongUtils/IntCong/index.html

Module CongUtils.IntCong

Types

Arithmetic utilities

Constructors

Predicates

Printing

Set operations

Forward operations

Filters

Backward operations

Reduction

dune-project
Dependency

Module `CongUtils.IntCong`