BL2Int converts boolean lists that are viewed as 2-complement representations of an integer to an F# integer i. Caution: The function may fail if bl cannot be represented with 32-bits.

BL2IntDecStr is an abbreviation for BL2IntDecStrSign "+" "-".

"BL2IntDecStrSign plus minus bl" expects a boolean list bl that is interpreted as 2-complement representation of an integer number X. The function then determines the radix-10 representation of X in terms of a string consisting of decimal digits 0,...,0. In addition, two strings "plus" and "minus" must be given that are used to prefix the generated string in case the number is non-negative or negative, respectively.

BL2Nat converts boolean lists that are viewed as radix-2 representations to a non-negative integer i. Caution: The function may fail if bl cannot be represented as a 32-bit integer.

Given a boolean list bl that is understood as binary representation of a natural number, BL2NatDecStr(bl) computes a string s that consists of decimal digits 0,...,9 that is the radix-10 representation of the the considered natural number.

BinBitConst2BL s expects a string like "0b1011" that represents a binary bitvector constant in Quartz. The prefix "0b" is then removed and the remaining string is converted to a boolean list by mapping 0 and 1 to false and true, respectively.

CeilLog2(n) is the least integer greater than or equal to log2(n). i.e., CeilLog2 n = int (ceil ((log (double n)) / (log 2.0)))

Div implements the mathematical definition of integer division, i.e. Div(x,y) is that number q where an integer r exists such that (1) x=q*y+r, (2) abs(r)

FloorLog2(n) is the greatest integer less than or equal to log2(n). i.e., FloorLog2 n = int (floor ((log (double n)) / (log 2.0)))

HexBitConst2BL s expects a string like "0x7342" that represents an hexadecimal bitvector constant in Quartz. The prefix "0x" is then removed and the remaining string is converted to a boolean list by mapping the hexadecimal digits to their corresponding radix-2 representations.

Int2BL converts any non-negative integer i to its 2-complement representation given as a boolean list.

IntDecStr2BL(s) expects a string s that must start with '+' or '-' and consists of decimal digits 0,...,9 otherwise. The string is is viewed as explicit sign radix-10 representation of an integer that is converted to its binary 2-complement representation.

Mod implements the positive remainder of integer division, i.e. Mod(x,y) is that number r where an integer q exists such that (1) x=q*y+r, (2) abs(r)

Nat2BL converts a non-negative integer i to its radix-2 representation given as a boolean list.

NatConstStr2BL s expects a string like "123u" that represents an unsigned integer in Quartz. The suffix "u" is then removed and the remaining string is converted by NatDecStr2BL to a radix-2 representation.

NatDecStr2BL(s) converts any string s that consists of decimal digits 0,...,9 that is viewed as radix-10 representation of a natural number to a boolean list such that is the radix-2 representation of the decimal number s.

OctBitConst2BL s expects a string like "0o7342" that represents an octal bitvector constant in Quartz. The prefix "0o" is then removed and the remaining string is converted to a boolean list by mapping the octal digits to their corresponding radix-2 representations.

extract the n-th bit of bitvector bl=[bL;...;b0] and fails if out of range

evaluate StaticBoolCase([(c1,b1);...,(cn,bn)],b), i.e. if one of the ci is true, then return the leftmost bi whose ci is true, otherwise return b

perform boolean conjunction: StaticBoolConj(b1,b2) = b1 && b2

perform boolean disjunction: StaticBoolDisj(b1,b2) = b1 || b2

perform boolean equivalence: StaticBoolEqu(b1,b2) = (b1=b2)

perform boolean implication: StaticBoolImpl(b1,b2) = (not b1) || b2

evaluate BoolIte: StaticBoolIte(b1,b2,b3) = if b1 then b2 else b3

perform boolean negation: StaticBoolNeg b = not b

perform boolean next: StaticBoolNext b = b

perform bitvector concatenation: StaticBtvAppend(bl1,bl2) = bl1@bl2

evaluate StaticBtvCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl

perform bitwise boolean conjunction, argument lists must have same length

perform bitwise boolean disjunction, argument lists must have same length

perform bitvector equality: StaticBtvEqu(bl1,bl2) = (bl1=bl2)

perform bitwise boolean equivalence, argument lists must have same length

perform bitwise boolean implication, argument lists must have same length

StaticBtvIte(b,bl1,bl2) = if b then bl1 else bl2

perform bitwise boolean negation

perform bitvector next: StaticBtvNext bl = bl

convert int constant to bitvector constant of given length (note that int constants are already stored as 2-complement bitvectors)

convert nat constant to bitvector constant of given length (note that nat constants are already stored as radix-2 bitvectors)

replicate a boolean constant to a bitvector: StaticBtvReplicate(b,n) = [b;...;b], where the generated bitvector has length n

perform bitvector reversal: StaticBtvReverse([bL;...;b0]) = [b0;...;bL]

extract a segment of a bitvector: StaticBtvSegment([bL;...;b0],n2,n1) = [bn2;...;bn1] where L>=n2>=n1>=0 must hold

sign-adjust length of bitector bv to n, i.e. first remove all redundant sign bits (i.e. bits that are equal to their right neighbor) to obtain a bitvector bv', then either replicate the leftmost bit to extend bv' to length n or remove further leading bits to reduce the size to n (which modifies int-constants)

perform sign-bit reduction, ie. remove all leading sign bits ie leftmost elements equal to their right neighbor

zero-adjust length of bitector bv to n, i.e. first remove all leading zero bits to obtain a bitvector bv', then either add zero bits to extend bv' to length n or remove further leading bits to reduce the size to n (which modifies nat-constants)

perform zero-bit reduction, ie. remove all leading zero bits (of course [false] is maintained as it is)

compute the absolute value of a 2-complement number which is given as radix-2 number representation, since used as NatExpr

addition of the 2-complement numbers bl1 and bl2

evaluate StaticIntCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl

quotient of division of the 2-complement numbers bl1 and bl2 has meaningless value when bl2 is [false]

StaticIntEqu(bl1,bl2) checks whether bl1 and bl2 represent the same the 2-complement number

StaticIntIte(b,bl1,bl2) = if b then bl1 else bl2

StaticIntLeq(bl1,bl2) checks whether bl1 is less than or equal to bl2 when these are evaluated as 2-complement numbers

StaticIntLes(bl1,bl2) checks whether bl1 is less than bl2 when these are evaluated as 2-complement numbers

remainder of division of the 2-complement numbers bl1 and bl2 has meaningless value when bl2 is [false]

multiplication of the 2-complement numbers bl1 and bl2

perform IntExpr next: StaticIntNext bl = bl

convert IntExpr constant to bitvector (note that IntExpr constants are already stored in 2-complement representation

bind 2-complement number, i.e. return bl if -blBound<=bl=blBound, and otherwise return -blBound (note that blBound is a radix-2 number while bl is a 2-complement number and that the result is of course also a 2-complement number)

subtraction of the 2-complement numbers bl1 and bl2

addition of the radix-2 numbers bl1 and bl2

evaluate StaticNatCase([(c1,bl1);...,(cn,bln)],bl), i.e. if one of the ci is true, then return the leftmost bli whose ci is true, otherwise return bl

quotient of division of the radix-2 numbers bl1 and bl2 has meaningless value when bl2 is [false]

StaticNatEqu(bl1,bl2) checks whether bl1 and bl2 represent the same the radix-2 number

exponentiation of the radix-2 numbers bl1 and bl2

StaticNatIte(b,bl1,bl2) = if b then bl1 else bl2

StaticNatLeq(bl1,bl2) checks whether bl1 is less than or equal to bl2 when these are evaluated as radix-2 numbers

StaticNatLes(bl1,bl2) checks whether bl1 is less than bl2 when these are evaluated as radix-2 numbers

log2 of a radix-2 number: it's the number of bits minus one after zero-reduction; this number is returned as radix-2 number; note that log2(0) is not defined

remainder of division of the radix-2 numbers bl1 and bl2 has meaningless value when bl2 is [false]

multiplication of the radix-2 numbers bl1 and bl2

perform NatExpr next: StaticNatNext bl = bl

convert NatExpr constant to bitvector (note that NatExpr constants are already stored in radix-2 representations

bind radix-2 number, i.e. return bl if bl

subtraction of the radix-2 numbers bl1 and bl2; has meaningless values when the radix-2 value of bl1 is less than bl2