Created
October 1, 2018 20:15
-
-
Save regehr/c8591f2e73ac4202b57ab0ef510887b9 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from z3 import * | |
# find autobiographical numbers | |
def auto(lim): | |
if lim < 1 or lim > 10: | |
raise Exception('only 1..10 are valid arguments') | |
print str(lim) + ":" | |
s = Solver() | |
vars = [] | |
for x in range(0, lim): | |
v = Int('X' + str(x)) | |
s.add(v >= 0, v < lim) | |
vars.append(v) | |
for x in range(0, lim): | |
sum = 0 | |
for y in range(0, lim): | |
sum = sum + If(vars[y] == x, 1, 0) | |
s.add(vars[x] == sum) | |
s.add(vars[0] != 0) | |
while True: | |
noRep = False | |
r = s.check() | |
if r == sat: | |
m = s.model() | |
for x in range(0, lim): | |
z = m[vars[x]] | |
noRep = Or(noRep, vars[x] != z.as_long()) | |
print z.as_long(), | |
s.add(noRep) | |
else: | |
print r | |
return | |
for i in range(1, 11): | |
auto(i) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment