DOMAINS :: SMT-LIB :: Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

[QPQ]

Forums QPQ
DOMAINS :: SMT-LIB ::.. Proposal for a theory of fixed-size bit-vectors in SMT-LIB format

silvio wrote at Mar 09, 2006 - 04:40 AM
---------------------------------------------------------------------
Here is another attempt to submit the proposal for the theory of
fixed-size bit-vectors.  Below, you will find my original message.

Silvio.

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

Dear All,

please find enclosed a first draft proposal of a formalization of 
a theory of fixed-size bit-vectors whose dimension is 4 (we can
easily generate theories for dimensions 8, 16, 32, 64, 128, etc).

In order to have a reasonable parsing of the benchmarks in the
theories, it is necessary to relax the requirements of the existing
SMT-LIB format in two respects:

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

 2) we allow a function symbol f to be overloaded when the sort of any
    term whose top-most symbol is f is uniquely determined by the
    sorts of its arguments.

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 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.
At the end of this message, you will find a more detailed explanation
of the problems that lead us to propose the above two extensions to
the actual SMT-LIB format.

If you are not too concerned with the details of the SMT-LIB format,
you can ignore (or, better, quickly read) much of the text entitled
"Details" and only have a look at the enclosed files which contain
both the theory and the logic for fixed-size bit-vectors.  Since the
theory is quite rich and the literature presents many variants, we
have tried to be as exhaustive as possible by including the largest
intersection among the formalizations we are able to find out in the
literature.

We encourage everyone interested in the theory to carefully look at
the attached files (containing both the theory for size 4 and the
related logic for benchmarks) and signal us omissions and unnecessary
operators which have been included.

We hope to start an interesting and fruitful discussion.

Best regards,

        Cesare and Silvio 

------------> bv4.theory   BitVec[1] BitVec[1])
        (>  BitVec[2] BitVec[2])
        (>  BitVec[3] BitVec[3])
        (>  BitVec[4] BitVec[4])
      )

 :type-constraints 
 "The set of well-sorted BitVec-terms is defined as follows:
   a term s is well-sorted BitVec-term iff 
   -- s is a constant symbol of sort BitVec[i] for 1 
---------------------------------------------------------------------

Reply to this message:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=reply&topic=179&forum=46

Browse thread:
http://www.qpq.org/modules.php?op=modload&name=phpBB_14&file=index&action=viewtopic&topic=179

You are receiving this Email because you are subscribed to be notified of events in forums at: http://www.qpq.org/