package dolmen

  1. Overview
  2. Docs
package dolmen
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.

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