(logic QF_BV
:smt-lib-version 2.6
:smt-lib-release "2017-11-24"
:written-by "Silvio Ranise, Cesare Tinelli, and Clark Barrett"
:date "2010-05-02"
:last-updated "2017-06-13"
:update-history
"Note: history only accounts for content changes, not release changes.
2020-05-20 bvxnor is no longer marked as left associative, as that is
inconsistent with its meaning as the negation of bvxor.
2017-06-13 Added that bvxor and bvxnor are left associative
2017-05-03 Updated to Version 2.6. Division and remainder operations are no
longer undefiend when the second operand is 0. See
the FixedSizeBitVectors theory definition for details.
2015-04-25 Updated to Version 2.5.
2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors.
2011-06-15 Fixed bug in definition of bvsmod. Previously, it gave an incorrect
answer when the divisor is negative and goes into the dividend evenly.
"
:theories (FixedSizeBitVectors)
:language
"Closed quantifier-free formulas built over an arbitrary expansion of the
FixedSizeBitVectors signature with free constant symbols over the sorts
(_ BitVec m) for 0 < m. Formulas in ite terms must satisfy the same
restriction as well, with the exception that they need not be closed
(because they may be in the scope of a let binder).
"
:notes
"For quick reference, the following is a brief and informal summary of the
legal symbols in this logic and their meaning (formal definitions are found
either in the FixedSizeBitvectors theory, or in the extensions below).
Defined in theory FixedSizeBitvectors:
Bitvector constants:
- #bX where X is a binary numeral of length m defines the
bitvector constant with value X and size m.
- #xX where X is a hexadecimal numeral of length m defines the
bitvector constant with value X and size 4*m.
Functions:
(concat (_ BitVec i) (_ BitVec j) (_ BitVec m))
- concatenation of bitvectors of size i and j to get a new bitvector of
size m, where m = i + j
((_ extract i j) (_ BitVec m) (_ BitVec n))
- extraction of bits i down to j from a bitvector of size m to yield a
new bitvector of size n, where n = i - j + 1
(bvnot (_ BitVec m) (_ BitVec m))
- bitwise negation
(bvand (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise and
(bvor (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise or
(bvneg (_ BitVec m) (_ BitVec m))
- 2's complement unary minus
(bvadd (_ BitVec m) (_ BitVec m) (_ BitVec m))
- addition modulo 2^m
(bvmul (_ BitVec m) (_ BitVec m) (_ BitVec m))
- multiplication modulo 2^m
(bvudiv (_ BitVec m) (_ BitVec m) (_ BitVec m))
- unsigned division, truncating towards 0
(bvurem (_ BitVec m) (_ BitVec m) (_ BitVec m))
- unsigned remainder from truncating division
(bvshl (_ BitVec m) (_ BitVec m) (_ BitVec m))
- shift left (equivalent to multiplication by 2^x where x is the value of
the second argument)
(bvlshr (_ BitVec m) (_ BitVec m) (_ BitVec m))
- logical shift right (equivalent to unsigned division by 2^x where x is
the value of the second argument)
(bvult (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for unsigned less-than
Defined below:
Functions:
(bvnand (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise nand (negation of and)
(bvnor (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise nor (negation of or)
(bvxor (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise exclusive or
(bvxnor (_ BitVec m) (_ BitVec m) (_ BitVec m))
- bitwise equivalence (equivalently, negation of bitwise exclusive or)
(bvcomp (_ BitVec m) (_ BitVec m) (_ BitVec 1))
- bit comparator: equals #b1 iff all bits are equal
(bvsub (_ BitVec m) (_ BitVec m) (_ BitVec m))
- 2's complement subtraction modulo 2^m
(bvsdiv (_ BitVec m) (_ BitVec m) (_ BitVec m))
- 2's complement signed division
(bvsrem (_ BitVec m) (_ BitVec m) (_ BitVec m))
- 2's complement signed remainder (sign follows dividend)
(bvsmod (_ BitVec m) (_ BitVec m) (_ BitVec m))
- 2's complement signed remainder (sign follows divisor)
(bvashr (_ BitVec m) (_ BitVec m) (_ BitVec m))
- 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.
The following symbols are parameterized by the numeral i, where i >= 1.
((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x
The following symbols are parameterized by the numeral i, where i >= 0.
((_ zero_extend i) (_ BitVec m) (_ BitVec m+i))
- ((_ zero_extend i) x) means extend x with zeroes to the (unsigned)
equivalent bitvector of size m+i
((_ sign_extend i) (_ BitVec m) (_ BitVec m+i))
- ((_ sign_extend i) x) means extend x to the (signed) equivalent bitvector
of size m+i
((_ rotate_left i) (_ BitVec m) (_ BitVec m))
- ((_ rotate_left i) x) means rotate bits of x to the left i times
((_ rotate_right i) (_ BitVec m) (_ BitVec m))
- ((_ rotate_right i) x) means rotate bits of x to the right i times
(bvule (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for unsigned less than or equal
(bvugt (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for unsigned greater than
(bvuge (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for unsigned greater than or equal
(bvslt (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for signed less than
(bvsle (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for signed less than or equal
(bvsgt (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for signed greater than
(bvsge (_ BitVec m) (_ BitVec m) Bool)
- binary predicate for signed greater than or equal
"
:extensions
"Below, let |exp| denote the integer resulting from the evaluation
of the arithmetic expression exp.
- Bitvector Constants:
(_ bvX n) where X and n are numerals, i.e. (_ bv13 32),
abbreviates the term #bY of sort (_ BitVec n) such that
[[#bY]] = nat2bv[n](X) for X=0, ..., 2^n - 1.
See the specification of the theory's semantics for a definition
of the functions [[_]] and nat2bv. Note that this convention implicitly
considers the numeral X as a number written in base 10.
- Bitwise operators
For all terms s,t of sort (_ BitVec m), where 0 < m,
(bvnand s t) abbreviates (bvnot (bvand s t))
(bvnor s t) abbreviates (bvnot (bvor s t))
(bvxor s t) abbreviates (bvor (bvand s (bvnot t)) (bvand (bvnot s) t))
(bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t)))
(bvcomp s t) abbreviates (bvxnor s t) if m = 1, and
(bvand (bvxnor ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
(bvcomp ((_ extract |m-2| 0) s) ((_ extract |m-2| 0) t))) otherwise.
Additionally, bvxor is left associative, so:
(bvxor s_1 s_2 ... s_n) abbreviates (bvxor (bvxor s_1 s_2 ...) s_n), and
- Arithmetic operators
For all terms s,t of sort (_ BitVec m), where 0 < m,
(bvsub s t) abbreviates (bvadd s (bvneg t))
(bvsdiv s t) abbreviates
(let ((?msb_s ((_ extract |m-1| |m-1|) s))
(?msb_t ((_ extract |m-1| |m-1|) t)))
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
(bvudiv s t)
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
(bvneg (bvudiv (bvneg s) t))
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
(bvneg (bvudiv s (bvneg t)))
(bvudiv (bvneg s) (bvneg t))))))
(bvsrem s t) abbreviates
(let ((?msb_s ((_ extract |m-1| |m-1|) s))
(?msb_t ((_ extract |m-1| |m-1|) t)))
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
(bvurem s t)
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
(bvneg (bvurem (bvneg s) t))
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
(bvurem s (bvneg t)))
(bvneg (bvurem (bvneg s) (bvneg t))))))
(bvsmod s t) abbreviates
(let ((?msb_s ((_ extract |m-1| |m-1|) s))
(?msb_t ((_ extract |m-1| |m-1|) t)))
(let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
(abs_t (ite (= ?msb_t #b0) t (bvneg t))))
(let ((u (bvurem abs_s abs_t)))
(ite (= u (_ bv0 m))
u
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
u
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
(bvadd (bvneg u) t)
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
(bvadd u t)
(bvneg u))))))))
(bvule s t) abbreviates (or (bvult s t) (= s t))
(bvugt s t) abbreviates (bvult t s)
(bvuge s t) abbreviates (or (bvult t s) (= s t))
(bvslt s t) abbreviates:
(or (and (= ((_ extract |m-1| |m-1|) s) #b1)
(= ((_ extract |m-1| |m-1|) t) #b0))
(and (= ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
(bvult s t)))
(bvsle s t) abbreviates:
(or (and (= ((_ extract |m-1| |m-1|) s) #b1)
(= ((_ extract |m-1| |m-1|) t) #b0))
(and (= ((_ extract |m-1| |m-1|) s) ((_ extract |m-1| |m-1|) t))
(bvule s t)))
(bvsgt s t) abbreviates (bvslt t s)
(bvsge s t) abbreviates (bvsle t s)
- Other operations
For all numerals i > 0, j > 1 and 0 < m, and all terms s and t of
sort (_ BitVec m),
(bvashr s t) abbreviates
(ite (= ((_ extract |m-1| |m-1|) s) #b0)
(bvlshr s t)
(bvnot (bvlshr (bvnot s) t)))
((_ repeat 1) t) stands for t
((_ repeat j) t) abbreviates (concat t ((_ repeat |j-1|) t))
((_ zero_extend 0) t) stands for t
((_ zero_extend i) t) abbreviates (concat ((_ repeat i) #b0) t)
((_ sign_extend 0) t) stands for t
((_ sign_extend i) t) abbreviates
(concat ((_ repeat i) ((_ extract |m-1| |m-1|) t)) t)
((_ rotate_left 0) t) stands for t
((_ rotate_left i) t) abbreviates t if m = 1, and
((_ rotate_left |i-1|)
(concat ((_ extract |m-2| 0) t) ((_ extract |m-1| |m-1|) t))
otherwise
((_ rotate_right 0) t) stands for t
((_ rotate_right i) t) abbreviates t if m = 1, and
((_ rotate_right |i-1|)
(concat ((_ extract 0 0) t) ((_ extract |m-1| 1) t)))
otherwise
"
)
