[SMT-LIB] Multiple representations

cok@frontiernet.net cok at frontiernet.net
Wed Oct 13 17:04:29 EDT 2010


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.

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, 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?

- David



More information about the SMT-LIB mailing list