Skip to content

Instantly share code, notes, and snippets.

@ties

ties/z3_distinct.py

Created October 31, 2017 09:57
Show Gist options
  • Save ties/f61c8ecaf91b23acacdc3b952ec31e7c to your computer and use it in GitHub Desktop.
Save ties/f61c8ecaf91b23acacdc3b952ec31e7c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
z3_distinct.py
from z3 import Solver, EnumSort, Const, Distinct
s = Solver()
Color, (red, green, blue) = EnumSort('Color', ['red', 'green', 'blue'])
a = Const('a', Color)
b = Const('b', Color)
s.add(Distinct(a, b))
s.check()
print(s.model())
# [b = green, a = red]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment