[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