package dolmen
val mk : string -> t
Create a bitvector litteral from a string representation. The string should only contain characters '0' or '1'.
Bitvector extraction, using in that order, the end (exclusive) and then the start (inclusive) position of the bitvector to extract.
Extend the given bitvector with its most significant bit repeated the given number of times.
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
.
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).
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)
.
Arithmetic multiplication on bitvectors, modulo the size of the bitvectors (see add
).
Arithmetic 2's complement signed division. (see smtlib's specification for more information).
Arithmetic 2's coplement signed remainder (sign follows dividend). (see smtlib's specification for more information).
Arithmetic 2's coplement signed remainder (sign follows divisor). (see smtlib's specification for more information).
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).
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)
.
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
Boolean arithmetic comparison (less than). ult s t
should return the true
term iff s < t
.
Boolean signed arithmetic comparison (less than). (See smtlib's specification for more information)