package dolmen

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

Module Const.BitvSource

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

Sourceval bitv : string -> t

Bitvetor literals.

Sourceval to_nat : int -> t

Conversion to integers.

Sourceval of_int : int -> t

Conversion from integers.

Sourceval concat : (int * int) -> t

Bitvector concatenation.

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

Bitvector extraction.

Sourceval repeat : (int * int) -> t

Bitvector repetition.

Sourceval zero_extend : (int * int) -> t

Bitvector extension with zeros.

Sourceval sign_extend : (int * int) -> t

Bitvector extension with its most significant.

Sourceval rotate_right : (int * int) -> t

Bitvector rotation to the right.

Sourceval rotate_left : (int * int) -> t

Bitvector rotation to the left.

Sourceval not : int -> t

Bitwise negation.

Sourceval and_ : int -> t

Bitwise conjunction.

Sourceval or_ : int -> t

Bitwise disjunction.

Sourceval nand : int -> t

Bitwise nand.

Sourceval nor : int -> t

Bitwise nor.

Sourceval xor : int -> t

Bitwise xor.

Sourceval xnor : int -> t

Bitwise xnor.

Sourceval comp : int -> t

Bitwise comparison.

Sourceval neg : int -> t

Arithmetic complement on bitvectors.

Sourceval add : int -> t

Arithmetic addition on bitvectors.

Sourceval sub : int -> t

Arithmetic substraction on bitvectors.

Sourceval mul : int -> t

Arithmetic multiplication on bitvectors.

Sourceval udiv : int -> t

Arithmetic euclidian integer division on bitvectors.

Sourceval urem : int -> t

Arithmetic euclidian integer remainder on bitvectors.

Sourceval sdiv : int -> t

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

Sourceval srem : int -> t

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

Sourceval smod : int -> t

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

Sourceval shl : int -> t

Logical shift left.

Sourceval lshr : int -> t

Logical shift right.

Sourceval ashr : int -> t

Arithmetic shift right.

Sourceval ult : int -> t

Boolean arithmetic comparison (less than).

Sourceval ule : int -> t

Boolean arithmetic comparison (less or equal than).

Sourceval ugt : int -> t

Boolean arithmetic comparison (greater than).

Sourceval uge : int -> t

Boolean arithmetic comparison (greater or equal than).

Sourceval slt : int -> t

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

Sourceval sle : int -> t

Boolean signed arithmetic comparison (less or equal than).

Sourceval sgt : int -> t

Boolean signed arithmetic comparison (greater than).

Sourceval 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