(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 " )