union_sort.py

# Copyright Microsoft Corporation 2019
# This example illustrates the use of union types
# from the Python API. It is given as an example
# as response to #2215.

from z3 import *

u = Datatype('IntOrString')
u.declare('IntV', ('int', IntSort()))
u.declare('StringV', ('string', StringSort()))
IntOrString = u.create()
StringV = IntOrString.StringV
IntV = IntOrString.IntV

print(IntV(1))
print(StringV(StringVal("abc")))
print(IntV(1).sort())
print(IntV(1) == StringV(StringVal("abc")))
s = String('s')
print(simplify(IntV(1) == StringV(s)))