dolmen_type

A typechecker for automated deduction languages
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen_type
Parameter #3 Dolmen_type . Bitv . Smtlib2 . Tff . T
val mk : string -> Type.T.t

Create a bitvector litteral from a string representation. The string should only contain characters '0' or '1'.

val concat : Type.T.t -> Type.T.t -> Type.T.t

Bitvector concatenation.

val extract : int -> int -> Type.T.t -> Type.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 -> Type.T.t -> Type.T.t

Repetition of a bitvector.

val zero_extend : int -> Type.T.t -> Type.T.t

Extend the given bitvector with the given numer of 0.

val sign_extend : int -> Type.T.t -> Type.T.t

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

val rotate_right : int -> Type.T.t -> Type.T.t

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

val rotate_left : int -> Type.T.t -> Type.T.t

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

val not : Type.T.t -> Type.T.t

Bitwise negation.

val and_ : Type.T.t -> Type.T.t -> Type.T.t

Bitwise conjunction.

val or_ : Type.T.t -> Type.T.t -> Type.T.t

Bitwise disjunction.

val nand : Type.T.t -> Type.T.t -> Type.T.t

nand s t abbreviates not (and_ s t).

val nor : Type.T.t -> Type.T.t -> Type.T.t

nor s t abbreviates not (or_ s t).

val xor : Type.T.t -> Type.T.t -> Type.T.t

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

val xnor : Type.T.t -> Type.T.t -> Type.T.t

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

val comp : Type.T.t -> Type.T.t -> Type.T.t

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

val neg : Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.T.t

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

val udiv : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic euclidian integer division on bitvectors.

val urem : Type.T.t -> Type.T.t -> Type.T.t

Arithmetic euclidian integer remainder on bitvectors.

val sdiv : Type.T.t -> Type.T.t -> Type.T.t

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

val srem : Type.T.t -> Type.T.t -> Type.T.t

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

val smod : Type.T.t -> Type.T.t -> Type.T.t

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

val shl : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.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 : Type.T.t -> Type.T.t -> Type.T.t

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

val ule : Type.T.t -> Type.T.t -> Type.T.t

Boolean arithmetic comparison (less or equal than).

val ugt : Type.T.t -> Type.T.t -> Type.T.t

Boolean arithmetic comparison (greater than).

val uge : Type.T.t -> Type.T.t -> Type.T.t

Boolean arithmetic comparison (greater or equal than).

val slt : Type.T.t -> Type.T.t -> Type.T.t

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

val sle : Type.T.t -> Type.T.t -> Type.T.t

Boolean signed arithmetic comparison (less or equal than).

val sgt : Type.T.t -> Type.T.t -> Type.T.t

Boolean signed arithmetic comparison (greater than).

val sge : Type.T.t -> Type.T.t -> Type.T.t

Boolean signed arithmetic comparison (greater or equal than).