[SMT-LIB] a couple of logic issues

[Leonardo de Moura]

Hi Clark,


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

I didn't find any benchmark in QF_IDL, QF_LIA, QF_LRA, and QF_RDL  
that uses
unary predicate symbols. I used the following regular expression  
during the
search:  ":extrapreds (([^ ]* [^ ]*))".

Leonardo