[SMT-LIB] a couple of logic issues

[Cesare Tinelli]

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