You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

17 lines
340 B

from z3 import *
iters = [ Int(f"x{i}") for i in range(20) ]
solver = Solver()
for n,x in enumerate(iters):
if n == 0:
solver.add(x == 1111)
else:
last = iters[n - 1]
solver.add(Or(x == last, (x * 2) == last, x == ((last * 3) + 1)))
solver.add(iters[-1] == 1)
print(solver.check())
print(solver.model())