[SMT-LIB] bitvector theory
Cesare Tinelli
tinelli at cs.uiowa.edu
Fri May 5 01:10:39 EDT 2006
Dear All,
please find enclosed a second draft proposal of a formalization of
the theory of fixed-size bit-vectors of length is 4 (we can easily
generate theories for lengths 8, 16, 32, 64, 128, etc). The proposal
takes into consideration the feedback that we have received so far.
From a previous message you might recall that to have a reasonable
parsing of the benchmarks in the theories, it is helpful to relax the
requirements of the existing SMT-LIB format.
Here are the updated extensions:
1) we allow sort and function symbols to be indexed with respect to a
finite set of non-negative integers,
2) we allow function and predicate symbols to be overloaded, with the
restriction that if a function symbol has two different arities they
cannot differ by their return sort only,
3) we add the informal (i.e., text values) attributes :sorts_descrition,
:funs_description, and :preds_description to complement, respectively,
the formal attributes :sorts, :funs, and :preds.
Extension 1 allows us to generate finitely many sort and function
symbols in a systematic and principled way.
Extension 2 allows us to avoid generating too many function/predicate
symbols. Indeed, such extensions allows an easier generation of the
benchmarks without complicating too much parsing and in particular the
check for well-sortedness of terms. The restriction on the overloading
of function symbols guarantees that every well-sorted terms has a unique
sort. Note that it also implies that constant symbols cannot be overloaded.
Extension 3, which is new wrt the first draft, allows us to specify the
value of an attribute like :sorts, :funs, or :preds, more concisely,
if only informally. It is meant to facilitate human reading, although it
does not replace the official, formal definition. The latter must be
present, perhaps at the end of the theory definition (see theory below).
Since the first draft of this proposal may not have reached you in its
entirety because of mail server problem, in the next message you will
find a more detailed section explaining the problems that led us to
propose the above extensions to the actual SMT-LIB format. That section
also explains how we addressed some of the suggestions or requests we
received after the first draft.
If you are not too concerned with the details of the SMT-LIB format,
you can ignore (or, better, quickly read) much of the next message, and
only take a look at the two sections below which define respectively the
theory and the related logic for fixed-size bit-vectors.
We thank those of you who provided their feedback so far, and encourage
everyone interested in the theory to carefully look at the revised
definitions and let us know of any mistakes, or send us any further
comments or suggestion.
Best regards,
Cesare and Silvio
--------------------- bv4.theory -------------------------------
(theory Fixed_Size_BitVectors[4]
:written_by {Silvio Ranise and Cesare Tinelli}
:date {04/05/2006}
:sorts-desc
"All sort symbols of the form BitVec[i],
where i is a numeral between 1 and 4, inclusive."
:funs
"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 <= 4
"
:funs
"All function symbols with arity of the form
(extract[i:j] BitVec[m] BitVec[n])
where
- i,j,m,n are numerals
- 4 >= m > i >= j >= 0,
- n = j-i+1.
"
:funs
"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, -}
- op1 is from {bvand, bvor, bvxor, -, bvadd, *}
- m is a numeral
- 0 < m <= 4
"
:preds
"All predicate symbols with arity of the form
(pred BitVec[m] BitVec[m])
where
- pred is from {<, <=, >=, >}
- m is a numeral
- 0 < m <= 4
"
:sorts ( BitVec[1] BitVec[2] BitVec[3] BitVec[4] )
:funs (
(bv0 BitVec[4]) (bv1 BitVec[4]))
(concat BitVec[1] BitVec[1] BitVec[2])
(concat BitVec[1] BitVec[2] BitVec[3])
(concat BitVec[1] BitVec[3] BitVec[4])
(concat BitVec[2] BitVec[1] BitVec[3])
(concat BitVec[2] BitVec[2] BitVec[4])
(concat BitVec[3] BitVec[1] BitVec[4])
(extract[0:0] BitVec[1] BitVec[1])
(extract[0:0] BitVec[2] BitVec[1])
(extract[1:0] BitVec[2] BitVec[2])
(extract[1:1] BitVec[2] BitVec[1])
(extract[0:0] BitVec[3] BitVec[1])
(extract[1:0] BitVec[3] BitVec[2])
(extract[2:0] BitVec[3] BitVec[3])
(extract[1:1] BitVec[3] BitVec[1])
(extract[2:1] BitVec[3] BitVec[2])
(extract[2:2] BitVec[3] BitVec[1])
(extract[0:0] BitVec[4] BitVec[1])
(extract[1:0] BitVec[4] BitVec[2])
(extract[2:0] BitVec[4] BitVec[3])
(extract[3:0] BitVec[4] BitVec[4])
(extract[1:1] BitVec[4] BitVec[1])
(extract[2:1] BitVec[4] BitVec[2])
(extract[3:1] BitVec[4] BitVec[3])
(extract[2:2] BitVec[4] BitVec[1])
(extract[3:2] BitVec[4] BitVec[2])
(extract[3:3] BitVec[4] BitVec[1])
(bvnot BitVec[1] BitVec[1])
(bvnot BitVec[2] BitVec[2])
(bvnot BitVec[3] BitVec[3])
(bvnot BitVec[4] BitVec[4])
(bvand BitVec[1] BitVec[1] BitVec[1])
(bvand BitVec[2] BitVec[2] BitVec[2])
(bvand BitVec[3] BitVec[3] BitVec[3])
(bvand BitVec[4] BitVec[4] BitVec[4])
(bvor BitVec[1] BitVec[1] BitVec[1])
(bvor BitVec[2] BitVec[2] BitVec[2])
(bvor BitVec[3] BitVec[3] BitVec[3])
(bvor BitVec[4] BitVec[4] BitVec[4])
(bvxor BitVec[1] BitVec[1] BitVec[1])
(bvxor BitVec[2] BitVec[2] BitVec[2])
(bvxor BitVec[3] BitVec[3] BitVec[3])
(bvxor BitVec[4] BitVec[4] BitVec[4])
(bvadd BitVec[1] BitVec[1] BitVec[1])
(bvadd BitVec[2] BitVec[2] BitVec[2])
(bvadd BitVec[3] BitVec[3] BitVec[3])
(bvadd BitVec[4] BitVec[4] BitVec[4])
(bvneg BitVec[1] BitVec[1])
(bvneg BitVec[2] BitVec[2])
(bvneg BitVec[3] BitVec[3])
(bvneg BitVec[4] BitVec[4])
(bvsub BitVec[1] BitVec[1] BitVec[1])
(bvsub BitVec[2] BitVec[2] BitVec[2])
(bvsub BitVec[3] BitVec[3] BitVec[3])
(bvsub BitVec[4] BitVec[4] BitVec[4])
(bvmul BitVec[1] BitVec[1] BitVec[1])
(bvmul BitVec[2] BitVec[2] BitVec[2])
(bvmul BitVec[3] BitVec[3] BitVec[3])
(bvmul BitVec[4] BitVec[4] BitVec[4])
)
:preds (
(<= BitVec[1] BitVec[1])
(<= BitVec[2] BitVec[2])
(<= BitVec[3] BitVec[3])
(<= BitVec[4] BitVec[4])
(< BitVec[1] BitVec[1])
(< BitVec[2] BitVec[2])
(< BitVec[3] BitVec[3])
(< BitVec[4] BitVec[4])
(>= BitVec[1] BitVec[1])
(>= BitVec[2] BitVec[2])
(>= BitVec[3] BitVec[3])
(>= BitVec[4] BitVec[4])
(> BitVec[1] BitVec[1])
(> BitVec[2] BitVec[2])
(> BitVec[3] BitVec[3])
(> BitVec[4] BitVec[4])
)
: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=1, ..., 4) 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 <= 4, 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 bv0 and bv1 of sort BitVec[4], then
[[bv0]] := \lambda x : [0...4). 0
[[bv1]] := \lambda x : [0...3). 1
- Function symbols for concatenation
[[(concat s t)]] := \lambda x : [0...n+m).
if (x<n) then [[s]](x) else [[t]](x-n)
where
s and t are terms of sort BitVec[n] and BitVec[m], respectively,
0 < n <= 4, 0 < m <= 4, and 0 < n+m <= 4.
- 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 <= 4.
- Function symbols for 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)
[[(bvxor s t)]] := \lambda x : [0...m).
if [[s]](x) = [[t]](x) then 0 else 1
where s and t are both of sort BitVec[m] and 0 < m <= 4.
- Function symbols for arithmetic operations
To define the semantics of the bitvector operators bvadd, bvsub,
bvneg, and bvmul, it is helpful to use these ancillary functions:
o bv2nat which takes a bitvector b: [0...m) --> {0,1}
with 0 < m <= 4, 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 <= 4, which takes an integer n in the range
[0...2^m) and returns the (unique) bitvector b: [0,...,m) -> {0,1}
such that
b(m-1)*2^{m-1} + ... + b(0)*2^0 = n MOD 2^m
where MOD is usual modulo operation.
[[(bvadd s t)]] := nat2bv[m](bv2nat(s) + bv2nat(t))
[[(bvsub s t)]] := nat2bv[m](bv2nat(s) - bv2nat(t))
[[(bvneg s)]] := nat2bv[m](2^m - bv2nat(s))
[[(bvmul s t)]] := nat2bv[m](bv2nat(s) * bv2nat(t))
where s and t are both of sort BitVec[m].
"
)
------------------ bv4.logic ----------------------------------
(logic QF_BV[4]
:written_by {Silvio Ranise and Cesare Tinelli}
:date {04/05/2006}
:theory Fixed_Size_BitVectors[4]
:language
"Closed quantifier-free formulas built over an arbitrary expansion
of the Fixed_Size_BitVectors[4] signature with free constant symbols
of sort BitVec[m] only, for 0 < m <= 4.
Formulas in ite terms must satisfy the same restriction as well,
with the exception that they need not be closed.
"
:extensions
"
Below, let |exp| denote the integer resulting from the evaluation of
the arithmetic expression exp.
- bit0 abbreviates (extract[0:0] bv0)
- bit1 abbreviates (extract[0:0] bv1)
For all numerals j with 0 < j <= 4,
- (fill[j] bit0) abbreviates (extract[|j-1|:0] bv0)
- (fill[j] bit1) abbreviates (extract[|j-1|:0] bv1)
- the string bv followed by a the numeral n (as in bv135) abbreviates
any term t of sort BitVec[4] built out only of the symbols in
{concat, bit0, bit1} such that
[[t]] = nat2bv[4](n) for n=0, ..., 15 (= 2^4 - 1).
See the specification of the theory's semantic for a definition of
the functions [[_]] and nat2bv.
Note that this convention implicitly considers the numeral n as a
number written in base 10.
- (bvnand s t) abbreviates (bvnot (bvand s t))
- (bvnor s t) abbreviates (bvnot (bvor s t))
For all numerals j and m with 1 < j <= m <= 4 and
all terms of s and t of sort BitVec[m],
- (shift_left0 t 0) stands for t
- (shift_left0 t j) abbreviates
bit0 if m = 1, and
(shift_left0 (concat (extract[|m-2|:0] t) bit0) |j-1|) otherwise
- (shift_left1 t 0) stands for t
- (shift_left1 t j) abbreviates
bit1 if m = 1, and
(shift_left1 (concat (extract[|m-2|:0] t) bit1) |j-1|) otherwise
- (shift_right0 t 0) stands for t
- (shift_right0 t j) abbreviates bit0 if m = 1 and
(shift_right0 (concat bit0 (extract[|m-1|:1] t)) |j-1|) otherwise
- (shift_right1 t 0) stands for t
- (shift_right1 t j) abbreviates bv1 if m = 1 and
(shift_right1 (concat bit1 (extract[|m-1|:1] t)) |j-1|) otherwise
- (repeat t 1) abbreviates t
- (repeat t i) abbreviates (concat t (repeat t |i-1|))
provided that i > 1 and i*m <= 4
- (rotate_left t 0) stands for t
- (rotate_left t j) abbreviates t if m = 1, and
(rotate_left
(concat (extract[|m-2|:0] t) (extract[|m-1|:|m-1|] t)
|j-1|) otherwise
- (rotate_right t 0) stands for t
- (rotate_right t j) abbreviates t if m = 1, and
(rotate_right
(concat (extract[0:0] t) (extract[|m-1|:1] t))
|j-1|) otherwise
"
)
More information about the SMT-LIB
mailing list