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

[Clark Barrett]

Again, responses are below, with apologies for the delayed response.

-Clark


On Sat, May 22, 2010 at 12:00 PM, Trevor Alexander HANSEN <
thansen at csse.unimelb.edu.au> wrote:

>
> Hello,
>
> 1) I'm updating the parser for our solver to the SMTLIB2 language, and
> aren't sure how to handle symbols that contain whitespace. A symbol
> can be a:
> "a sequence of printable ASCII characters, including white
> spaces, that starts and ends with | and does not otherwise contain | ."
>
> Elsewhere:
> "There is no distinction between line breaks, tabs, and spaces---all
> are treated as whitespace."
>
> So the obvious question is whether the symbol: |\t| is the same as | | ? I
> expect they are different, and that likewise |\t\t| is different from
> |\t| ?
>

Whitespace within symbols defined using a pair of vertical bars does matter:
|\t| is different from || and |\t\t|.
Note also the recent post by Cesare which clarifies that the vertical bars
themselves are *not* part of the defined symbol (for compliance with the
LISP standard)

2) I'm uncertain about how to handle bit-vector division by zero. Signed
> division is defined as:
>
> (bvsdiv s t) abbreviates
>       (let ((?msb_s ((_ extract |m-1| |m-1|) s))
>             (?msb_t ((_ extract |m-1| |m-1|) t)))
>         (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
>              (bvudiv s t)
>         (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
>              (bvneg (bvudiv (bvneg s) t))
>         (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
>              (bvneg (bvudiv s (bvneg t)))
>              (bvudiv (bvneg s) (bvneg t))))))
>
> So:
>  (and (= (bvsdiv #x5 #x0) #x1) (= (bvsdiv #xb #x0) #x1))
>
> is defined as equivalent to:
> (and (= (bvudiv #x5 #x0) #x1) (= (bvneg (bvudiv (bvneg #xb) #0)) #x1))
>
> which simplifies to:
> (and (= (bvudiv #x5 #x0) #x1) (= (bvudiv #x5 #x0)) #xF))
>
> which is unsatisfiable and perhaps surprising (to me anway)? It seems
> nicest to have a special case for division by zero for each of bvsdiv,
> bvsrem, and bvsmod, so that function congruence can be handled without
> reference to bvudiv/bvurem.
>

If you look at the note at the bottom of the fixed-size bitvector theory,
you will see that SMT-LIB makes no assumptions at all about how division by
zero is defined for the built-in operators.  This means that benchmarks that
depend on a particular definition of division by zero may have different
answers depending on the solver.  The conclusion is that division by zero
should be guarded and benchmarks that depend on division by zero should not
be used to compare solvers (in fact - such benchmarks are not used in the
competition).  For these reasons, it doesn't seem worth the trouble to
distinguish the zero case in the derived operators.  If the behavior you see
above seems funny, it is just one of many ways in which division by zero is
funny and that is why it should be avoided.


> 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.