[SMT-LIB] a couple of logic issues

[Clark Barrett]

Hi folks,

As I've been double-checking the new benchmarks added to SMT-LIB, I've stumbled
across a couple of issues I want to get some feedback on.

1) The official description of the logic QF_UFIDL requires that terms beginning
   with + or - have a positive numeral as one of their two operands.  I noticed
   that some of the benchmarks use a negative numeral (these are benchmarks
   that we have had for some time--apparently no one has noticed this
   before).  Because these benchmarks have been there for a while and the use
   of a negative numeral is, I believe, still within the desired scope of the
   logic, I am inclined to suggest we augment the logic to allow negative
   constants, but I am interested in what other people think.

2) The other issue that I am unclear about is which logics allow the use of new
   unary predicate symbols.  Currently, it seems that we have benchmarks in all
   divisions that declare unary predicates using the "extrapreds" command.
   However, if I read the logics, it seems that QF_IDL and QF_RDL definitely do
   not allow unary predicates and some of the others are vague (i.e. they allow
   "free constant symbols").  What do people think about this?  Should all
   logics allow new unary predicats?  If not, does that mean that only the "UF"
   flavors of logics should allow declaration of unary predicates?

-Clark