[SMT-LIB] Questions: UF in QF_AUFBV, defn of symbols, bit-vector division.

[Morgan Deters]

Hi Trevor,

On Wed, Jun 16, 2010 at 04:34:36PM -0400, Clark Barrett wrote:
> > 3) This year's competition will use a fuzzer to produce check problems. In
> > the QF_AUFBV division as far as I'm aware there are no problems that use
> > UF. Our solver doesn't support UF. If benchmarks are added that use
> > UF, then I'll add it to the solver. However, if there are no problems
> > with UF come the competition, it'd be nice not to have the fuzzer generate
> > such problems?
> 
> This is really a question for the SMT-COMP list, not the SMT-LIB list.  Let
> me take it up with the other organizers and see what they think.

To follow up, after discussion with the other SMT-COMP organizers, we
have decided to create division QF_ABV, and move QF_AUFBV benchmarks
to that division (as none uses UF).

We intend to have a formal QF_ABV logic definition posted at the
smtlib.org web site soon.

This has the following consequences:

1. Solvers supporting arrays and bitvectors, but not UF, can safely
   enter without fear of problems from the fuzzer.

2. Entrants must recognize the string "QF_ABV" as a valid SMT-LIB
   logic.

3. Historical solvers (e.g., last year's winner) running in the
   competition don't support SMT-LIBv2 and may not recognize the
   string "QF_ABV" in SMT-LIBv1 benchmarks.  Thus the SMT-LIBv1
   benchmarks they solve will be part of the QF_ABV division but will
   contain a :logic attribute of QF_AUFBV.  This doesn't affect this
   year's entrants, which are required to handle the SMT-LIB v2
   benchmarks.

Thanks,
Morgan (also for the other organizers)
-- 
Morgan Deters
mdeters at cs.nyu.edu