title: Sort inheritance in z3
body: <p>Is there any way to define inheritance between sorts in z3? (I'm using the Python API)</p>
  
  <p>I'm trying to model two different types of events, write events and read events; for each of them I use a Sort (<strong>WriteSort</strong> and <strong>ReadSort</strong>). However I would like to have a "sum" Sort (<strong>EventSort</strong>) that is either a write or a read event.</p>
  
  <p>I'm defining functions with the following domain:</p>
  
  <pre><code>f1 = Function('f1', WriteSort, WriteSort, BoolSort())
  f2 = Function('f2', ReadSort, ReadSort, BoolSort())
  f3 = Function('f3', EventSort, EventSort, BoolSort())
  </code></pre>
  
  <p>One possibility would be to define <strong>EventSort</strong> as and abstract datatype, but then the domain of all my functions should be (<strong>EventSort x EventSort</strong>) and the only way I see to restrict such domain is doing it manually.</p>
  
  <p>Is there anyway to define both <strong>WriteSort</strong> and <strong>ReadSort</strong> as "subsort" of <strong>EventSort</strong>?</p>