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

[Trevor Alexander HANSEN]

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

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.

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?

Sorry in advance if these are answered somewhere already.

Thanks,

Trevor