1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
# 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)))
|
