package dolmen

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

A module for bit vector constant symbols that occur in terms.

val bitv : string -> t

Bitvetor literals.

val to_nat : int -> t

Conversion to integers.

val of_int : int -> t

Conversion from integers.

val concat : (int * int) -> t

Bitvector concatenation.

val extract : (int * int * int) -> t

Bitvector extraction.

val repeat : (int * int) -> t

Bitvector repetition.

val zero_extend : (int * int) -> t

Bitvector extension with zeros.

val sign_extend : (int * int) -> t

Bitvector extension with its most significant.

val rotate_right : (int * int) -> t

Bitvector rotation to the right.

val rotate_left : (int * int) -> t

Bitvector rotation to the left.

val not : int -> t

Bitwise negation.

val and_ : int -> t

Bitwise conjunction.

val or_ : int -> t

Bitwise disjunction.

val nand : int -> t

Bitwise nand.

val nor : int -> t

Bitwise nor.

val xor : int -> t

Bitwise xor.

val xnor : int -> t

Bitwise xnor.

val comp : int -> t

Bitwise comparison.

val neg : int -> t

Arithmetic complement on bitvectors.

val add : int -> t

Arithmetic addition on bitvectors.

val sub : int -> t

Arithmetic substraction on bitvectors.

val mul : int -> t

Arithmetic multiplication on bitvectors.

val udiv : int -> t

Arithmetic euclidian integer division on bitvectors.

val urem : int -> t

Arithmetic euclidian integer remainder on bitvectors.

val sdiv : int -> t

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

val srem : int -> t

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

val smod : int -> t

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

val shl : int -> t

Logical shift left.

val lshr : int -> t

Logical shift right.

val ashr : int -> t

Arithmetic shift right.

val ult : int -> t

Boolean arithmetic comparison (less than).

val ule : int -> t

Boolean arithmetic comparison (less or equal than).

val ugt : int -> t

Boolean arithmetic comparison (greater than).

val uge : int -> t

Boolean arithmetic comparison (greater or equal than).

val slt : int -> t

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

val sle : int -> t

Boolean signed arithmetic comparison (less or equal than).

val sgt : int -> t

Boolean signed arithmetic comparison (greater than).

val sge : int -> t

Boolean signed arithmetic comparison (greater or equal than).

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