diff options
Diffstat (limited to 'docs/SMT-COMP')
| -rw-r--r-- | docs/SMT-COMP/BitVector_ArraysEx.smt | 74 | ||||
| -rw-r--r-- | docs/SMT-COMP/BitVectors.smt | 187 | ||||
| -rw-r--r-- | docs/SMT-COMP/QF_AUFBV.smt | 19 | ||||
| -rw-r--r-- | docs/SMT-COMP/QF_BV.smt | 261 |
4 files changed, 541 insertions, 0 deletions
diff --git a/docs/SMT-COMP/BitVector_ArraysEx.smt b/docs/SMT-COMP/BitVector_ArraysEx.smt new file mode 100644 index 00000000..a60413ca --- /dev/null +++ b/docs/SMT-COMP/BitVector_ArraysEx.smt @@ -0,0 +1,74 @@ +(theory BitVector_ArraysEx + + :written_by {Clark Barrett} + :date {May 7, 2007} + +:sorts_description { + All sort symbols of the form BitVec[m], + where m is a numeral greater than 0. + + All sort symbols of the form Array[m:n], + where m and n are numerals with m > 0 and n > 0. +} + +:funs_description { + All functions from the theory Fixed_Size_Bitvectors. +} + +:funs_description { + All function symbols with arity of the form + + (select Array[m:n] BitVec[m] BitVec[n]) + + where + - m,n are numerals + - m > 0, n > 0 +} + +:funs_description { + All function symbols with arity of the form + + (store Array[m:n] BitVec[m] BitVec[n] Array[m:n]) + + where + - m,n are numerals + - m > 0, n > 0 +} + +:preds_description { + All predicates from the theory Fixed_Size_Bitvectors. +} + + + :definition + "This is a theory containing an infinite number of copies of the theory of + functional arrays with extensionality: one for each pair of bitvector sorts. + It can be formally defined as the union of the SMT-LIB theory + Fixed_Size_Bitvectors and an infinite number of variants of the SMT-LIB + theory ArraysEx: one for each distinct signature morphism mapping the sort Index + to BitVec[m] and the sort Element to Bitvec[n] where m and n range over all + positive numerals. In each of the copies of ArraysEx, the sort Array is + renamed to Array[m:n] and each copy of ArraysEx contributes exactly one select + function and one store function to the infinite polymorphic family of select + and store functions described above. + " + + :notes + "As in the theory Fixed_Size_Bitvectors, this theory does not + provide a value for the formal attributes :sorts, :funs, and :preds because + there are an infinite number of them. See the notes in theory + Fixed_Size_Bitvectors for details. + + If for i=1,2, T_i is an SMT-LIB theory with sorts S_i, function symbols F_i, + predicate symbols P_i, and axioms A_i, by \"union\" of T_1 and T_2 + we mean the theory T with sorts S_1 U S_2, function symbols F_1 U F_2, + predicate symbols P_1 U P_2, and axioms A_1 U A_2 (where U stands for set + theoretic union). + + The theory T is a well-defined SMT-LIB theory whenever S_1, S_2, F_1, F_2, + P_1, P_2 are all pairwise disjoint, as is the case for the component theories + considered here. + " +) + + diff --git a/docs/SMT-COMP/BitVectors.smt b/docs/SMT-COMP/BitVectors.smt new file mode 100644 index 00000000..f2cde1b3 --- /dev/null +++ b/docs/SMT-COMP/BitVectors.smt @@ -0,0 +1,187 @@ +(theory Fixed_Size_BitVectors + +:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett} + +:date {May 7, 2007} + +:notes + "Against the requirements of the current SMT-LIB standard this theory does + not provide a value for the formal attributes :sorts, :funs, and :preds. + The reason is that the theory has an infinite number of sort, function, and + predicate symbols, and so they cannot be specified formally in the current + SMT-LIB language. While extending SMT-LIB's type system with dependent + types would allow a finitary formal specification of all the symbols in + this theory's signature, such an extension does not seem to be worth the + trouble at the moment. As a temporary ad-hoc solution, this theory + declaration specifies the signature, in English, in the user-defined + attributes :sorts_description, :funs_description, and :preds_description. + " + +:sorts_description { + All sort symbols of the form BitVec[m], + where m is a numeral greater than 0. +} + +:funs_description { + Constant symbols bit0 and bit1 of sort BitVec[1] +} + +:funs_description { + All function symbols with arity of the form + + (concat BitVec[i] BitVec[j] BitVec[m]) + + where + - i,j,m are numerals + - i,j > 0 + - i + j = m +} + +:funs_description { + All function symbols with arity of the form + + (extract[i:j] BitVec[m] BitVec[n]) + + where + - i,j,m,n are numerals + - m > i >= j >= 0, + - n = i-j+1. +} + +:funs_description { + All function symbols with arity of the form + + (op1 BitVec[m] BitVec[m]) + or + (op2 BitVec[m] BitVec[m] BitVec[m]) + + where + - op1 is from {bvnot, bvneg} + - op2 is from {bvand, bvor, bvadd, bvmul, bvudiv, bvurem, bvshl, bvlshr} + - m is a numeral greater than 0 +} + +:preds_description { + All predicate symbols with arity of the form + + (pred BitVec[m] BitVec[m]) + + where + - pred is from {bvult} + - m is a numeral greater than 0 +} + +:definition + "This is a core theory for fixed-size bitvectors where the operations + of concatenation and extraction of bitvectors as well as the usual + logical and arithmetic operations are overloaded. + The theory is defined semantically as follows. + + The sort BitVec[m] (for m > 0) is the set of finite functions + whose domain is the initial segment of the naturals [0...m), meaning + that 0 is included and m is excluded, and the co-domain is {0,1}. + + The semantic interpretation [[_]] of well-sorted BitVec-terms is + inductively defined as follows. + + - Variables + + If v is a variable of sort BitVec[m] with 0 < m, then + [[v]] is some element of [{0,...,m-1} -> {0,1}], the set of total + functions from {0,...,m-1} to {0,1}. + + - Constant symbols bit0 and bit1 of sort BitVec[1] + + [[bit0]] := \lambda x : [0,1). 0 + [[bit1]] := \lambda x : [0,1). 1 + + - Function symbols for concatenation + + [[(concat s t)]] := \lambda x : [0...n+m). + if (x<m) then [[t]](x) else [[s]](x-m) + where + s and t are terms of sort BitVec[n] and BitVec[m], respectively, + 0 < n, 0 < m. + + - Function symbols for extraction + + [[(extract[i:j] s)]] := \lambda x : [0...i-j+1). [[s]](j+x) + where s is of sort BitVec[l], 0 <= j <= i < l. + + - Bit-wise operations + + [[(bvnot s)]] := \lambda x : [0...m). if [[s]](x) = 0 then 1 else 0 + + [[(bvand s t)]] := \lambda x : [0...m). + if [[s]](x) = 0 then 0 else [[t]](x) + + [[(bvor s t)]] := \lambda x : [0...m). + if [[s]](x) = 1 then 1 else [[t]](x) + + where s and t are both of sort BitVec[m] and 0 < m. + + - Arithmetic operations + + To define the semantics of the bitvector arithmetic operators, we first + introduce some additional definitions: + + o (x div y) where x and y are integers with x >= 0 and y > 0 returns the + integer part of x divided by y (i.e., truncated integer division). + + o (x rem y) where x and y are integers with x >= 0 and y > 0 returns the + remainder when x is divided by y. Note that we always have the following + equivalence (for y > 0): (x div y) * y + (x rem y) = x. + + o bv2nat which takes a bitvector b: [0...m) --> {0,1} + with 0 < m, and returns an integer in the range [0...2^m), + and is defined as follows: + + bv2nat(b) := b(m-1)*2^{m-1} + b(m-2)*2^{m-2} + ... + b(0)*2^0 + + o nat2bv[m], with 0 < m, which takes a non-negative integer + n and returns the (unique) bitvector b: [0,...,m) -> {0,1} + such that + + b(m-1)*2^{m-1} + ... + b(0)*2^0 = n rem 2^m + + Now, we can define the following operations. Suppose s and t are both terms + of sort BitVec[m], m > 0. + + [[(bvneg s)]] := nat2bv[m](2^m - bv2nat([[s]])) + + [[(bvadd s t)]] := nat2bv[m](bv2nat([[s]]) + bv2nat([[t]])) + + [[(bvmul s t)]] := nat2bv[m](bv2nat([[s]]) * bv2nat([[t]])) + + [[(bvudiv s t)]] := if bv2nat([[t]]) != 0 then + nat2bv[m](bv2nat([[s]]) div bv2nat([[t]])) + + [[(bvurem s t)]] := if bv2nat([[t]]) != 0 then + nat2bv[m](bv2nat([[s]]) rem bv2nat([[t]])) + + - Shift operations + + Suppose s and t are both terms of sort BitVec[m], m > 0. We make use of the + definitions given for the arithmetic operations, above. + + [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]]))) + + [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]]))) + + Finally, we can define the binary predicate bvult: + + (bvult s t) is interpreted to be true iff bv2nat([[s]]) < bv2nat([[t]]) + + Note that the semantic interpretation above is underspecified because it + does not specify the meaning of (bvudiv s t) or (bvurem s t) in case + bv2nat([[t]]) is 0. Since the semantics of SMT-LIB's underlying logic + associates *total* functions to function symbols, we then consider as models + of this theory *any* interpretation conforming to the specifications above + (and defining bvudiv and bvurem arbitrarily when the second argument + evaluates to 0). Benchmarks using this theory should only include a + :status sat or :status unsat attribute if the status is independent of + the particular choice of model for the theory. + + " + +) diff --git a/docs/SMT-COMP/QF_AUFBV.smt b/docs/SMT-COMP/QF_AUFBV.smt new file mode 100644 index 00000000..bc055c35 --- /dev/null +++ b/docs/SMT-COMP/QF_AUFBV.smt @@ -0,0 +1,19 @@ +(logic QF_AUFBV + + :written_by {Clark Barrett} + :date {May 7, 2007} + + :theory BV_ArraysEx + + :language + "Closed quantifier-free formulas built over an arbitrary expansion of the + BV_ArraysEx signature with free function and predicate symbols over + the sorts of BV_ArraysEx. 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 expression). + " + :extensions + "As in the logic QF_BV." +) + + diff --git a/docs/SMT-COMP/QF_BV.smt b/docs/SMT-COMP/QF_BV.smt new file mode 100644 index 00000000..edf02241 --- /dev/null +++ b/docs/SMT-COMP/QF_BV.smt @@ -0,0 +1,261 @@ +(logic QF_BV + +:written_by {Silvio Ranise, Cesare Tinelli, and Clark Barrett} +:date {May 7, 2007} + +:theory Fixed_Size_BitVectors + +:language + + "Closed quantifier-free formulas built over an arbitrary expansion of the + Fixed_Size_BitVectors 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 expression). + " + +: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 Fixed_Size_Bitvectors theory, or in the extensions below). + + Defined in theory Fixed_Size_Bitvectors: + + Functions/Constants: + + (bit0 BitVec[1]) + - the constant consisting of a single bit with value 0 + (bit1 BitVec[1]) + - the constant consisting of a single bit with value 1 + (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 (undefined if divisor is 0) + (bvurem BitVec[m] BitVec[m] BitVec[m]) + - unsigned remainder from truncating division (undefined if divisor is 0) + (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) + + Predicates: + + (bvult BitVec[m] BitVec[m]) + - binary predicate for unsigned less than + + Defined below: + + Functions/Constants: + + Bitvector constants: + - bvX[m] where X is a numeral in base 10 defines the bitvector constant + with numeric value X of size m. + - bvbinX where X is a binary numeral of length m defines the + bitvector constant with value X and size m. + - bvhexX where X is a hexadecimal numeral of length m defines the + bitvector constant with value X and size 4*m. + (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 bit1 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 >= 0. + + (repeat[i] BitVec[m] BitVec[i*m]) + - (repeat[i] x) means concatenate i copies of x + (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 y times + + Predicates: + + (bvule BitVec[m] BitVec[m]) + - binary predicate for unsigned less than or equal + (bvugt BitVec[m] BitVec[m]) + - binary predicate for unsigned greater than + (bvuge BitVec[m] BitVec[m]) + - binary predicate for unsigned greater than or equal + (bvslt BitVec[m] BitVec[m]) + - binary predicate for signed less than + (bvsle BitVec[m] BitVec[m]) + - binary predicate for signed less than or equal + (bvsgt BitVec[m] BitVec[m]) + - binary predicate for signed greater than + (bvsge BitVec[m] BitVec[m]) + - 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: + The string bv followed by the numeral n and a size [m] (as in bv13[32]) + abbreviates any term t of sort BitVec[m] built only out of the symbols in + {concat, bit0, bit1} such that + + [[t]] = nat2bv[m](n) for n=0, ..., 2^m - 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 n as a number written in base 10. + + For backward compatibility, if the size [m] is omitted, then the size is + assumed to be 32. + + The string bvbin followed by a sequence of 0's and 1's abbreviates the + concatenation of a similar sequence of bit0 and bit1 terms. Thus, + if n is the numeral represented in base 2 by the sequence of 0's and 1's + and m is the length of the sequence, then the term represents + nat2bv[m](n). For example bvbin0101 is equivalent to bv5[4]. + + The string bvhex followed by a sequence of digits and/or letters from A to + F is interpreted similarly as a concatenation of bit0 and bit1 as follows. + If n is the numeral represented in hexadecimal (base 16) by the sequence of + digits and letters from A to F and m is four times the length of the + sequence, then the term represents nat2bv[m](n). For example, bvbinFF is + equivalent to bv255[8]. Letters in the hexadecimal sequence may be in + either upper or lower case. + + - 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 + + - 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)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvudiv s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvudiv (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvneg (bvudiv s (bvneg t))) + (bvudiv (bvneg s) (bvneg t))))))) + (bvsrem s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvneg (bvurem (bvneg s) t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvurem s (bvneg t))) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + (bvsmod s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvadd (bvneg (bvurem (bvneg s) t)) t) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvadd (bvurem s (bvneg t)) t) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + (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) bit1) + (= (extract[|m-1|:|m-1|] t) bit0)) + (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) bit1) + (= (extract[|m-1|:|m-1|] t) bit0)) + (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 j > 1 and 0 < m, and all terms of s and t of + sort BitVec[m], + + (bvashr s t) abbreviates + (ite (= (extract[|m-1|:|m-1|] s) bit0) + (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[j] t) abbreviates (concat (repeat[j] bit0) t) + + (sign_extend[0] t) stands for t + (sign_extend[j] t) abbreviates + (concat (repeat[j] (extract[|m-1|:|m-1|] t)) t) + + (rotate_left[0] t) stands for t + (rotate_left[j] t) abbreviates t if m = 1, and + (rotate_left[|j-1|] + (concat (extract[|m-2|:0] t) (extract[|m-1|:|m-1|] t)) + otherwise + + (rotate_right[0] t) stands for t + (rotate_right[j] t) abbreviates t if m = 1, and + (rotate_right[|j-1|] + (concat (extract[0:0] t) (extract[|m-1|:1] t))) + otherwise + + " +) + |