[SMT-LIB] Built-in name for Booleans
tinelli at cs.uiowa.edu
Mon Nov 23 20:06:34 EST 2009
Fowarding the message below from Tjark in response to Nikolaj's
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.
More information about the SMT-LIB