package dolmen

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

Satisfy the required interface for typing smtlib bitvectors.

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

Bitvector concatenation.

val 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.

val repeat : int -> t -> t

Repetition of a bitvector.

val zero_extend : int -> t -> t

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

val sign_extend : int -> t -> t

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

val rotate_right : int -> t -> t

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

val rotate_left : int -> t -> t

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

val not : t -> t

Bitwise negation.

val and_ : t -> t -> t

Bitwise conjunction.

val or_ : t -> t -> t

Bitwise disjunction.

val nand : t -> t -> t

nand s t abbreviates not (and_ s t).

val nor : t -> t -> t

nor s t abbreviates not (or_ s t).

val xor : t -> t -> t

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

val xnor : t -> t -> t

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

val comp : t -> t -> t

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

val 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.

val 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).

val 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).

val mul : t -> t -> t

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

val udiv : t -> t -> t

Arithmetic euclidian integer division on bitvectors.

val urem : t -> t -> t

Arithmetic euclidian integer remainder on bitvectors.

val sdiv : t -> t -> t

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

val srem : t -> t -> t

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

val smod : t -> t -> t

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

val 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).

val 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).

val 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

val ult : t -> t -> t

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

val ule : t -> t -> t

Boolean arithmetic comparison (less or equal than).

val ugt : t -> t -> t

Boolean arithmetic comparison (greater than).

val uge : t -> t -> t

Boolean arithmetic comparison (greater or equal than).

val slt : t -> t -> t

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

val sle : t -> t -> t

Boolean signed arithmetic comparison (less or equal than).

val sgt : t -> t -> t

Boolean signed arithmetic comparison (greater than).

val 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
val to_nat : t -> t

Application of the bv2nat conversion function.

val 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
val mk : string -> t

Bitvector litteral.

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