mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
20 lines
543 B
Python
20 lines
543 B
Python
# 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)))
|