package dolmen

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Term.BitvSource

Satisfy the required interface for typing smtlib bitvectors.

include Dolmen_intf.Term.Smtlib_Bitv with type t := t
Sourceval concat : t -> t -> t

Bitvector concatenation.

Sourceval extract : int -> int -> t -> t

Bitvector extraction, using in that order, the end (exclusive) and then the start (inclusive) position of the bitvector to extract.

Sourceval repeat : int -> t -> t

Repetition of a bitvector.

Sourceval zero_extend : int -> t -> t

Extend the given bitvector with the given number of 0s.

Sourceval sign_extend : int -> t -> t

Extend the given bitvector with its most significant bit repeated the given number of times.

Sourceval rotate_right : int -> t -> t

rotate_right i x means rotate bits of x to the right i times.

Sourceval rotate_left : int -> t -> t

rotate_left i x means rotate bits of x to the left i times.

Sourceval not : t -> t

Bitwise negation.

Sourceval and_ : t -> t -> t

Bitwise conjunction.

Sourceval or_ : t -> t -> t

Bitwise disjunction.

Sourceval nand : t -> t -> t

nand s t abbreviates not (and_ s t).

Sourceval nor : t -> t -> t

nor s t abbreviates not (or_ s t).

Sourceval xor : t -> t -> t

xor s t abbreviates or_ (and_ s (not t)) (and_ (not s) t).

Sourceval xnor : t -> t -> t

xnor s t abbreviates or_ (and_ s t) (and_ (not s) (not t)).

Sourceval comp : t -> t -> t

Bitwise comparison. comp s t equals #b1 iff s and t are bitwise equal.

Sourceval neg : t -> t

Arithmetic complement on bitvectors. Supposing an input bitvector of size m representing an integer k, the resulting term should represent the integer 2^m - k.

Sourceval add : t -> t -> t

Arithmetic addition on bitvectors, modulo the size of the bitvectors (overflows wrap around 2^m where m is the size of the two input bitvectors).

Sourceval sub : t -> t -> t

Arithmetic substraction on bitvectors, modulo the size of the bitvectors (2's complement subtraction modulo). sub s t should be equal to add s (neg t).

Sourceval mul : t -> t -> t

Arithmetic multiplication on bitvectors, modulo the size of the bitvectors (see add).

Sourceval udiv : t -> t -> t

Arithmetic euclidian integer division on bitvectors.

Sourceval urem : t -> t -> t

Arithmetic euclidian integer remainder on bitvectors.

Sourceval sdiv : t -> t -> t

Arithmetic 2's complement signed division. (see smtlib's specification for more information).

Sourceval srem : t -> t -> t

Arithmetic 2's complement signed remainder (sign follows dividend). (see smtlib's specification for more information).

Sourceval smod : t -> t -> t

Arithmetic 2's complement signed remainder (sign follows divisor). (see smtlib's specification for more information).

Sourceval shl : t -> t -> t

Logical shift left. shl t k return the result of shifting t to the left k times. In other words, this should return the bitvector representing t * 2^k (since bitvectors represent integers using the least significatn bit in cell 0).

Sourceval lshr : t -> t -> t

Logical shift right. lshr t k return the result of shifting t to the right k times. In other words, this should return the bitvector representing t / (2^k).

Sourceval ashr : t -> t -> t

Arithmetic shift right, like logical shift right except that the most significant bits of the result always copy the most significant bit of the first argument

Sourceval ult : t -> t -> t

Boolean arithmetic comparison (less than). ult s t should return the true term iff s < t.

Sourceval ule : t -> t -> t

Boolean arithmetic comparison (less or equal than).

Sourceval ugt : t -> t -> t

Boolean arithmetic comparison (greater than).

Sourceval uge : t -> t -> t

Boolean arithmetic comparison (greater or equal than).

Sourceval slt : t -> t -> t

Boolean signed arithmetic comparison (less than). (See smtlib's specification for more information)

Sourceval sle : t -> t -> t

Boolean signed arithmetic comparison (less or equal than).

Sourceval sgt : t -> t -> t

Boolean signed arithmetic comparison (greater than).

Sourceval sge : t -> t -> t

Boolean signed arithmetic comparison (greater or equal than).

Satisfy the required interface for typing smtlib bv2nat.

include Dolmen_intf.Term.Smtlib_Bvconv with type t := t
Sourceval to_nat : t -> t

Application of the bv2nat conversion function.

Sourceval of_int : int -> t -> t

Application of the int2bv conversion function.

Satisfy the required interface for typing smtlib floats.

include Dolmen_intf.Term.Smtlib_Float_Bitv with type t := t
Sourceval mk : string -> t

Bitvector litteral.

OCaml

Innovation. Community. Security.