[SMT-LIB] a couple of logic issues

[Clark Barrett]

OK.  If it seems that there are no objections to allowing Boolean variables in
all of the logics, then I think the logics need to specifiy that.  I went and
reviewed the language in the SMT-LIB standard and it seems quite clear that any
use of "extrapreds" must be sanctioned in the "language" attribute of the
logic.

-Clark

> 
> Clark Barrett wrote:
> > 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.
> >
> As far as I can tell, allowing Boolean variables in a logic that already 
> allows Boolean combinations of literals is always unproblematic from a 
> practical point of view: the mechanism one needs to deal with the 
> Boolean operators can be used to deal with the Boolean variables as 
> well. (Does anyone have a difference experience?)
> If a logic only allows conjunctions of literals, dealing with variables 
> is even easier. So I think in general we could allow Boolean variables 
> in any SMT-LIB logic.
> 
> 
> Cesare
> 
> 
> > -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
> >>
> > 
> > _______________________________________________
> > SMT-LIB mailing list
> > SMT-LIB at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>