[SMT-LIB] Multiple representations

[Cesare Tinelli]

Hi David,

On 13 Oct 2010, at 16:04, cok at frontiernet.net wrote:

> Given a new sort symbols, e.g. (declare-sort ZZZ 0) and (declare-sort YYY 1)
> section 4.1 of the SMT-LIB document says that ZZZ is a sort (because the sort symbol ZZZ has arity 0), but YYY is not.
> 
That is correct. In the same way as a function symbol of arity 0 is a term but one of arity > 0 is not.


> Point 2 under section 4.1 says that (YYY Int) would be a sort.  My question is whether (ZZZ) is also a sort by this rule. 

> The case n=0 is not explicitly excluded, 

If you are referring to point 2 of Definition 1, the n there is meant to be > 0. I'll add the missing constraint. However, even as given, there is no ambiguity---only redundancy. See below.


> but we end up with two equivalent representations: ZZZ and (ZZZ).
> Similarly in section 4.2.2, it would appear that with (declare-fun c () Bool)
> both  c  and (c) are well-sorted terms of sort Bool.
> Is this intended?
> 

Section 4 defines an abstract syntax for SMT-LIB 2, for the purposes of providing a formal semantics. In the abstract syntax, parentheses are meta symbols, so ZZZ and (ZZZ) are the same thing indeed, and so are c and (c). The parentheses in these cases are just unnecessary (meta) notation.

I suspect however that you are wondering whether in the *concrete* syntax (ZZZ) is a sort, and if so, how it relates to ZZZ. Now, in the concrete syntax the expression (ZZZ) is not a sort (see Section 3.5). Similarly, again in the concrete syntax, the expression (c) is not a term (see Section 3.5). So there is no ambiguity there.

I hope this clarifies your doubts.


Cesare



> - David
> 
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib