Module Relations.Additive

Simple additive relation: y = delta*x + b where delta is +/- 1 (indicated by a boolean with true -> positive)

• On integer is is the usual unbounded addition
• On bitvector it is modulo addition
• On boolean is is simply negation

type delta =

1. | PlusOne
2. | MinusOne

type (_, _) t = private

1. | Identity : ('a, 'a) t
2. | Add_Modulo : {
   1. factor : delta;
   2. size : Units.In_bits.t;
   3. amount : Z.t;
   } -> (Operator.Function_symbol.bitvector, Operator.Function_symbol.bitvector) t
   (*

   Invariant: is not identity either factor is MinusOne or amount is non-zero (modulo 2^size) amount is in -2^(size-1) .. 2^(size-1)-1

   *)
3. | Add_Unbounded : delta * Z.t -> (Operator.Function_symbol.integer, Operator.Function_symbol.integer) t
   (*

   Invariant: is not identity either the delta is MinusOne (negation) or the value is non-zero

   *)
4. | Bool_Not : (Operator.Function_symbol.boolean, Operator.Function_symbol.boolean) t
   (*

   see Additive for description of this relation

   The type is made private to ensure invariant are respected, use the constructors below to build terms

   *)

val additive_identity : ('a, 'a) t

val additive_bitvector : size:Units.In_bits.t -> delta -> Z.t -> (Operator.Function_symbol.bitvector, Operator.Function_symbol.bitvector) t

val additive_integer : delta -> Z.t -> (Operator.Function_symbol.integer, Operator.Function_symbol.integer) t

val boolean_not : (Operator.Function_symbol.boolean, Operator.Function_symbol.boolean) t

include Union_Find.Parameters.GENERIC_GROUP with type ('a, 'b) t := ('a, 'b) t

include Union_Find.Parameters.GENERIC_MONOID with type ('a, 'b) t := ('a, 'b) t

val equal : ('a, 'b) t -> ('a, 'b) t -> bool

Equality of relations

val pretty : Stdlib.Format.formatter -> ('a, 'b) t -> unit

Pretty printer for relations

val pretty_with_terms : (Stdlib.Format.formatter -> 'tl -> unit) -> 'tl -> (Stdlib.Format.formatter -> 'tr -> unit) -> 'tr -> Stdlib.Format.formatter -> ('a, 'b) t -> unit

pretty_with_terms pp_x x pp_y y rel pretty-prints the relation rel between terms x and y (respectively printed with pp_x and pp_y).

For placeholder variables, use pretty

val identity : ('a, 'a) t

The identity relation

val compose : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t

Monoid composition, written using the functional convention compose f g is f \circ g. Should be associative, and compatible with identity:

• For all x, G.compose x G.identity = G.compose G.identity x = x
• For all x y z, G.compose x (G.compose y z) = G.compose (G.compose x y) z

val inverse : ('a, 'b) t -> ('b, 'a) t

Group inversion, should verify for all x: G.compose x (G.inverse x) = G.compose (G.inverse x) x = G.identity

module Action (B : Single_value_abstraction.Sig.NUMERIC_ENUM) : GROUP_ACTION with type bitvector = B.bitvector and type integer = B.integer and type boolean = B.boolean and type enum = B.enum and type ('a, 'b) relation = ('a, 'b) t