[SMT-LIB] bitvector theory

Fri May 5 01:26:21 EDT 2006

Dear all,

here follow details and rationales for the proposed formalization of the 
theory of bit vectors and the related SMT-LIB extensions.

Best,

Silvio and Cesare

---------------------------------------------------------------------------

To have a reasonable parsing of the benchmarks in the theory
of fixed-size bit-vectors, it is necessary to relax the requirements of
the existing SMT-LIB format in two respects:

  1) we allow sort, function, and predicate symbols to be indexed with
     respect to a finite set of non-negative integers, and

  2) we allow a function or predicate symbol f to be overloaded as long
     as the sort of any term whose top-most symbol is f is uniquely
     determined by the sorts of its arguments. (This is achieved by not
     allowing in a theory the declarations of a function with two arities
     that differ only for the return sort.)

------------------------------------------------------------------------
BRIEF DIGRESSION
Since the indexing mechanism of ) and 2) creates long lists of sort,
function, and predicate symbols, to ameliorate the human readability
of the theory specification, we consider a variant of the :sorts, :funs
and :preds attributes obtained by post-fixing "_description" to each one
of them, which will contain a text value meant to be in addition (but,
not in substitution) of the formal one in the :sorts, :funs and :preds
attributes.  Although, it is not necessary to have distinct attribute
names, we prefer this solution since the new attributes can be
considered as unsupported by current parsers.
However, it is up to the theory specifier to insert such attributes
together with suitable texts in order to ease the human reading of
the theory.
END OF BRIEF DIGRESSION
------------------------------------------------------------------------

Extension 1) allows us to generate finitely many sort, function, and
predicate symbols in a systematic and principled way.  Extension 2)
allows us to avoid generating too many function symbols.

Let us illustrate the situation with an example.

Consider the original SMT-LIB format, i.e. simple many-sorted
first-order logic, and the problem of formalizing the theory of fixed
bit-vectors whose size is 8.

First of all, we need to introduce enough sort symbols to represent
bit-vectors of size 1, of size 2, ..., up to size 8.  For example, we
can consider the following set of sort symbols:

               BitVec_1, BitVec_2, ..., and BitVec_8.

Then, consider the operation of concatenating two bit-vectors: we need
to introduce a function symbol for

  - concatenating bit-vectors of size 1 with bit-vectors of size 1,
  - concatenating bit-vectors of size 1 with bit-vectors of size 2,
  - ...
  - concatenating bit-vectors of size 2 with bit-vectors of size 1,
  - concatenating bit-vectors of size 2 with bit-vectors of size 2,
  - ...
  - concatenating bit-vectors of size 7 with bit-vectors of size 1,

i.e, we need to introduce the following set of function symbols:

  concat_1_1, concat_1_2, ..., concat_2_1, concat_2_2, ..., concat_7_1.

We can more succinctly describe the set of function symbol above as
follows:

            concat_i_j where 0 < i, j <= 8 and i+j<=8.

We need to introduce 28 (= number of pairs (i,j) such that i+j <= 8
when i and j takes values between 1 and 8) function symbols!

We have a similar (if not worse) situation when considering the
operating of extracting a part of a bit-vector by identifying a lower
and an upper index: we need to introduce a function symbol for

  - extracting the sub-bit-vector between 0 and 0 (i.e a bit-vector of
    size 1) out of a bit-vector of size 1,
  - extracting the sub-bit-vector between 0 and 0 (i.e a bit-vector of
    size 1) out of a bit-vector of size 2,
  - ...
  - extracting the sub-bit-vector between 0 and 1 (i.e a bit-vector of
    size 2) out of a bit-vector of size 2,
  - extracting the sub-bit-vector between 0 and 1 (i.e a bit-vector of
    size 1) out of a bit-vector of size 3,
  - ...
  - extracting the sub-bit-vector between 1 and 1 (i.e a bit-vector of
    size 1) out of a bit-vector of size 1,
  - extracting the sub-bit-vector between 1 and 1 (i.e a bit-vector of
    size 1) out of a bit-vector of size 2,
  - ...
  - extracting the sub-bit-vector between 7 and 7 (i.e a bit-vector of
    size 1) out of a bit-vector of size 8,

i.e., we need to introduce the following set of function symbols:

  extract_0_0_1, extract_0_0_2, ..., extract_0_1_2, extract_0_1_3, ...,
  extract_1_1_1, extract_1_1_2, ..., ...., extract_7_7_8.

We can describe the set of function symbol above as follows:

       extract_i_j_n where 0 <= i <= j < n <= 8

We need to introduce too many function symbols, around 960!

Now, let us analyze how extensions 1) and 2) above allow us to
dramatically reduce the number of symbols while improving readability
without complicating parsing and especially the check for
well-sortedness.

First, all the symbols we have introduced above are indexed by some
finite set of non-negative integers.  So, following convention 1)
above, we make this explicit by, for example, introducing the
following set of sort symbols where indexes are put between square
parentheses:

               BitVec[1], BitVec[2], ..., and BitVec[8].

In this way, it is clear that there are exactly 8 sort symbols and we
can easily retrieve the index while parsing the compound identifiers.
It is worth noticing that this does not change the background
framework, which is still that of many-sorted first-order logic since
we require that the range of an index to be a finite set of
non-negative integers.  Since, only finitely many sort symbols can be
generated this way, we can easily extend many-sorted first-order logic
to accommodate this extension which is nothing more than a convenient
syntactic mechanism.

With reference to the brief digression above, it is worth noticing
that the set of sort symbols introduced above can be compactly
described with help of some (very) simple arithmetic constraints:

               BitVector[i] with 1 <= i <= 8.

In our proposal, this more declarative and compact way of describing
the set of symbols built by the newly introduced indexing mechanism
can be captured by the (unsupported) attribute :sorts_description as 
follows:

:sorts_description
   "All sort symbols of the form BitVec[i],
    where i is a numeral between 1 and 8, inclusive."

Now, let us consider concatenation.  While working with the original
SMT-LIB format, we were forced to introduce 28 distinct function
symbols to describe essentially the same operation.  Indeed, we can
apply extension 1) above and more compactly describe such 28 function
symbols as follows:

               concat[m:n] where 0 < m, n <= 8 and m+n <= 8

But in this way, we keep getting 28 distinct function symbols even if
described in a more compact and elegant way.  The key observation here
is that whenever we have an application of the function concat[m:n] to
a term s as first argument and t as second argument, we already know
the value of m and the value of n since, to be well-sorted, s must be
of sort BitVec[m] and t must be of sort BitVec[n].  As a consequence,
we can drop indices m and n appended to concat and overload just one
function symbol, say concat: because of the previous observation we
will always be able to determine whether an application of concat is
well-sorted or not.  So, thanks to extension 2) above, we can more
compactly declare the function symbol for concatenation as follows:

              (concat BitVec[m] BitVec[n] BitVec[m+n])

where 0 < m, n <= 8 and m+n <= 8.

Let us turn our attention to the operation of extraction.  For such an
operation, it is no more true that as soon as we determine the sort of
the term representing the bit-vector from which we select a part, we
are capable of determining the sort of the result.  To this end, we
need also to consider the lower and upper indices of the selection.
As a consequence, we can exploit both extension 1) and extension 2)
above in order to reduce the set of function symbols denoting
extraction to a reasonable number as follows:

               (extract[i:j] BitVec[m] BitVec[j-i+1])

where 0 <= i < j < m <= 8.  In this way, for example, we have just one
(overloaded) function symbol to denote the extraction of the
bit-vector of size 1 at index 0 (up to index 0) for bit-vectors of
size 1, 2, 3, ..., and 8.  Similarly, we will have one (overloaded)
function symbols to denote the extraction of the bit-vectors of size 2
at index 0 (and up to index 1) for bit-vectors of size 2, 3, ...,
8. This cuts down the number of fresh function symbols to 120 (compare
with the 960 above with the old SMT-LIB format).

Again, we notice that the capability of introducing function symbols
indexed by a finite numbers of non-negative integers or some Cartesian
products of such finite sets is only a convenient syntactic mechanism
to introduce finitely many function symbols without augmenting the
expressiveness of many-sorted first-order logic which is the formal
framework underlying the SMT-LIB format.

Furthermore, notice that using extensions 1) and 2) above, it is
particularly easy to parse and check the well-sortedness of
expressions by exploiting the ability of accessing to the indexes of
the compound identifiers and evaluating simple (ground) arithmetic
expressions.  For example, the rule to check the well-sortedness of a
term of the form

                         (concat s t)

can be simply:

  if s is of sort BitVec[m] and t is of sort BitVec[n],
  then (concat s t) is of sort BitVec[m+n],
  provided that m+n <= 8
  (for the theory of fixed size bit-vectors whose dimension is 8)

Similarly, the rule to check the well-sortedness of a term of the form

	                (extract[i:j] s)

can be simply:

  if s is of sort BitVec[m] and 0 <= i <= j < 8,
  then (extract[i:j] s) is of sort BitVec[j-i+1]
  (for the theory of fixed size bit-vectors whose dimension is 8).

------------------------------------------------------------------------
NOTE ON EXTENSION 2)

As it is specified, extension 2) allows the theory specifier to use
the same symbol in many different theories.  For example, the binary
symbol + can be used both in some fragment of the theory of Arithmetic
(e.g., the theory Ints in the list of SMT-LIB theories) and in some
theory of bit-vectors.  In principle, as explained above, this should
not be problematic for parsing since it is always possible to
disambiguate the situation by looking at the sorts of the arguments to
each the symbol + is applied to.  However, on the basis of pragmatic
arguments (i.e., minimal modifications to already available parsing
routines), we prefer to restrict the overloading in a given theory or,
equivalently, to prevent the use of the same symbols in more than one
theory.  This should allow programmers to implement the overloading
mechanism described above only to disambiguate symbols in the new
theories of bit-vectors.  As a consequence, we propose to use bvadd
for addition of two bit-vectors, bvmult for their multiplication, and
so on.  In this way, the set of symbols for the arithmetic operation
over bit-vectors will be disjoint of the set of symbols for the "real"
arithmetic operations in the fragments of Arithmetic considered in the
list of SMT-LIB theories such as Ints.

END OF NOTE ON EXTENSION 2)
------------------------------------------------------------------------