[SMT-LIB] extensions to bitvector theory

[Clark Barrett]

> > > [Domagoj Babic wrote:]
> > > BTW, what does "packet" mean in egt benchmarks?
> >
> > [Clark Barrett wrote:]
> > I'm not sure.  These benchmarks came from verification work at Stanford,
> > submitted by Vijay Ganesh.  "packet" is probably a variable name for an array
> > used to model transactions or something similar.
> 
> Heh, Vijay said he had no clue, and that I should ask you Clark :-)
> 
> If it is an uninterpreted function, that means that all modular
> arithmetic theorem provers have to handle UIFs as well.
> 
> Quote from egt_0083.smt benchmark:
> packet def: :extrafuns ((packet BitVec[32] BitVec[8]))
> usage: (packet (extract[31:0] bv241))

I thought you were referring to the meaning of "packet" in the application that
produced the benchmark.  I don't know much about that.

However, I can elaborate on the meaning within the benchmark.  The "extrafuns"
construct introduces a new "uninterpreted" function symbol beyond those
available in the theory and logic.  So, yes, for these benchmarks, solvers have
to be able to handle both bitvectors and uninterpreted functions (thus the
division name QF_UFBV32).

> IMHO, the theory of modular arithmetic should be separate from UIFs.
> Modular arithmetic is already hard enough. Any converter requiring
> UIFs can do conversion before dumping benchmarks to SMT MA format.

The reason for our decision to include UF's last year is very simple.  We
didn't have any challenging benchmarks without UF's.  Our general philosophy
for SMT-LIB and SMT-COMP is to advertise for interesting benchmarks and then
have competition divisions based on the benchmarks we get.  If we get
challenging benchmarks and at least a couple of solvers for a division, then it
is a candidate for the competition.

If you would like to have a division *without* uninterpreted functions, then I
suggest you 1) help us get some benchmarks without uninterpreted functions; and
2) make a suggestion on the smt-comp at cs.nyu.edu mailing list

-Clark