[SMT-LIB] a couple of logic issues

[Clark Barrett]

You are right.  Sorry.  I meant 0-ary predicates (i.e. Boolean variables).  The
question is whether we should *always* allow additional Boolean variables or
only in some logics.

-Clark

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