package smtml

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

Module M_with_make.Bitv

val v : string -> int -> term

v s n constructs a bitvector term from the string s of width n.

val neg : term -> term

neg t constructs the negation of the bitvector term t.

val lognot : term -> term

lognot t constructs the bitwise NOT of the bitvector term t.

val to_int : signed:bool -> term -> term

to_int ~signed t convertes the bitvector term t into an integer.

val add : term -> term -> term

add t1 t2 constructs the sum of the bitvector terms t1 and t2.

val sub : term -> term -> term

sub t1 t2 constructs the difference of the bitvector terms t1 and t2.

val mul : term -> term -> term

mul t1 t2 constructs the product of the bitvector terms t1 and t2.

val div : term -> term -> term

div t1 t2 constructs the quotient of the bitvector terms t1 and t2.

val div_u : term -> term -> term

div_u t1 t2 constructs the unsigned quotient of the bitvector terms t1 and t2.

val logor : term -> term -> term

logor t1 t2 constructs the bitwise OR of the bitvector terms t1 and t2.

val logand : term -> term -> term

logand t1 t2 constructs the bitwise AND of the bitvector terms t1 and t2.

val logxor : term -> term -> term

logxor t1 t2 constructs the bitwise XOR of the bitvector terms t1 and t2.

val shl : term -> term -> term

shl t1 t2 constructs the left shift of t1 by t2.

val ashr : term -> term -> term

ashr t1 t2 constructs the arithmetic right shift of t1 by t2.

val lshr : term -> term -> term

lshr t1 t2 constructs the logical right shift of t1 by t2.

val smod : term -> term -> term

smod t1 t2 two's complement signed remainder (sign follows divisor).

val rem : term -> term -> term

rem t1 t2 constructs the remainder of the bitvector terms t1 and t2.

val rem_u : term -> term -> term

rem_u t1 t2 constructs the unsigned remainder of the bitvector terms t1 and t2.

val rotate_left : term -> term -> term

rotate_left t1 t2 constructs the left rotation of t1 by t2.

val rotate_right : term -> term -> term

rotate_right t1 t2 constructs the right rotation of t1 by t2.

val nego : term -> term

nego t constructs a predicate that checks that whether the bit-wise negation of t does not overflow.

val addo : signed:bool -> term -> term -> term

addo ~signed t1 t2 constructs a predicate that checks whether the bitwise addition of t1 and t2 does not overflow.

The signed argument is a boolean:

  • true -> for signed addition
  • false -> for unsigned addition
val subo : signed:bool -> term -> term -> term

subo ~signed t1 t2 constructs a predicate that checks whether the bitwise subtraction of t1 and t2 does not overflow.

The signed argument is a boolean:

  • true -> for signed subtraction
  • false -> for unsigned subtraction
val mulo : signed:bool -> term -> term -> term

mulo ~signed t1 t2 constructs a predicate that checks whether the bitwise multiplication of t1 and t2 does not overflow.

The signed argument is a boolean:

  • true -> for signed multiplication
  • false -> for unsigned multiplication
val divo : term -> term -> term

divo t1 t2 constructs a predicate that checks whether the bitwise division of t1 and t2 does not overflow.

val lt : term -> term -> term

lt t1 t2 constructs the less-than relation between bitvector terms t1 and t2.

val lt_u : term -> term -> term

lt_u t1 t2 constructs the unsigned less-than relation between bitvector terms t1 and t2.

val le : term -> term -> term

le t1 t2 constructs the less-than-or-equal relation between bitvector terms t1 and t2.

val le_u : term -> term -> term

le_u t1 t2 constructs the unsigned less-than-or-equal relation between bitvector terms t1 and t2.

val gt : term -> term -> term

gt t1 t2 constructs the greater-than relation between bitvector terms t1 and t2.

val gt_u : term -> term -> term

gt_u t1 t2 constructs the unsigned greater-than relation between bitvector terms t1 and t2.

val ge : term -> term -> term

ge t1 t2 constructs the greater-than-or-equal relation between bitvector terms t1 and t2.

val ge_u : term -> term -> term

ge_u t1 t2 constructs the unsigned greater-than-or-equal relation between bitvector terms t1 and t2.

val concat : term -> term -> term

concat t1 t2 constructs the concatenation of the bitvector terms t1 and t2.

val extract : term -> high:int -> low:int -> term

extract t ~high ~low extracts a bit range from t between high and low.

val zero_extend : int -> term -> term

zero_extend n t zero-extends the bitvector term t by n bits.

val sign_extend : int -> term -> term

sign_extend n t sign-extends the bitvector term t by n bits.