[SMT-LIB] Built-in name for Booleans

[Cesare Tinelli]

Fowarding the message below from Tjark in response to Nikolaj's  
question.


Cesare


PS:  A reminder to everybody: you must send email to his list from  
your registered address, otherwise it will be discarded.


Begin forwarded message:

> From: smt-lib-bounces at cs.nyu.edu
> Date: 23 November 2009 11:12:45 CST
> To: smt-lib-owner at cs.nyu.edu
> Subject: Auto-discard notification
>
> The attached message has been automatically discarded.
> From: Tjark Weber <tw333 at cam.ac.uk>
> Date: 23 November 2009 11:12:39 CST
> To: Nikolaj Bjorner <nbjorner at microsoft.com>
> Cc: "smt-lib at cs.nyu.edu" <smt-lib at cs.nyu.edu>, Arie Gurfinkel <arie at cmu.edu 
> >
> Subject: Re: [SMT-LIB] Built-in name for Booleans
>
>
> On Mon, 2009-11-23 at 16:52 +0000, Nikolaj Bjorner wrote:
>> The SMT-LIB 1 standard does not include a built-in name for Booleans.
>> Is there a known plan for a name: Bool, bool, Boolean?
>> (FWIW, Z3 uses "bool", making nice injustice to Mr. George Boole).
>
> The Version 2 draft that was posted to the SMT-LIB list by Cesare
> Tinelli in July uses "Bool".
>
> | 2) We drop the distinction between terms and formulas but we
> | introduce a distinguished Bool sort, always interpreted as the
> | Booleans, for what were formulas before.
>
> Best,
> Tjark
>
>
>