Uninterpreted datatype in Z3

Question

I'd like to create an uninterpreted datatype in Z3 lets call it "A". According to z3 documentations, I can declare it by using "DeclareSort" as follows:

A = DeclareSort('A')
a, b = Consts('a b', A)
s = Solver()
s.add(a != b)
s.check()

However I've seen some people using the following:

A = Datatype('Event')
A.declare('A0')
A = A.create()

a, b = Consts('a b', A) 

My question is that what is the difference between those two and which one is correct to declare new uninterpreted datatype. Also I could not understand what does A.declare('A0') means in the second part.

Answer 1

The Event datatype contains just one element called A0, so you should use the first suggestion to use DeclareSort.