Created
May 14, 2015 11:12
-
-
Save summerlight/28c6036cf6a38ef772cf to your computer and use it in GitHub Desktop.
division
This file contains hidden or 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
| import z3 | |
| z3.init("some_path") | |
| def flatten(v, i, j): | |
| formula = 0 | |
| for k in range(0, j - i): | |
| formula += pow(10, k) * v[j - k - 1] | |
| return formula | |
| def interval(val, i, j): | |
| return z3.And(i <= val, val <= j) | |
| def decimal(v): | |
| return [interval(i, 0, 9) for i in v] | |
| n = z3.IntVector('n', 8) | |
| d = z3.Int('d') | |
| q = z3.IntVector('q', 5) | |
| i0 = z3.IntVector('i0', 3) | |
| i1 = z3.IntVector('i1', 4) | |
| i2 = z3.IntVector('i2', 4) | |
| s = z3.Solver() | |
| equations = [ | |
| interval(d, 100, 999), | |
| q[1] == 7, | |
| q[3] == 0, | |
| interval(d * q[0], 1000, 9999), | |
| interval(d * q[1], 100, 999), | |
| interval(d * q[2], 100, 999), | |
| interval(d * q[4], 1000, 9999), | |
| i0[2] == n[4], | |
| i1[3] == n[5], | |
| i2[2] == n[6], | |
| i2[3] == n[7], | |
| flatten(n, 0, 4) - (d * q[0]) == flatten(i0, 0, 2), | |
| flatten(i0, 0, 3) - (d * q[1]) == flatten(i1, 0, 3), | |
| flatten(i1, 0, 4) - (d * q[2]) == flatten(i2, 0, 2), | |
| flatten(i2, 0, 4) == (d * q[4]) | |
| ] | |
| z3.solve(decimal(n) + decimal(q) + decimal(i0) + decimal(i1) + decimal(i2) + equations) |
This file contains hidden or 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
| [d = 122, | |
| i2__3 = 8, | |
| i2__2 = 9, | |
| i2__1 = 0, | |
| i2__0 = 1, | |
| i1__3 = 0, | |
| i1__2 = 2, | |
| i1__1 = 6, | |
| i1__0 = 0, | |
| i0__2 = 6, | |
| i0__1 = 1, | |
| i0__0 = 9, | |
| q__4 = 9, | |
| q__2 = 5, | |
| q__0 = 9, | |
| n__7 = 8, | |
| n__6 = 9, | |
| n__5 = 0, | |
| n__4 = 6, | |
| n__3 = 9, | |
| n__2 = 8, | |
| n__1 = 1, | |
| n__0 = 1, | |
| q__3 = 0, | |
| q__1 = 7] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment