1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103
| from z3 import *
res = [0x4F17, 0x9CF6, 0x8DDB, 0x8EA6, 0x6929, 0x9911, 0x40A2, 0x2F3E, 0x62B6, 0x4B82, 0x486C, 0x4002, 0x52D7, 0x2DEF, 0x28DC, 0x640D, 0x528F, 0x613B, 0x4781, 0x6B17, 0x3237, 0x2A93, 0x615F, 0x50BE, 0x598E, 0x4656, 0x5B31, 0x313A, 0x3010, 0x67FE, 0x4D5F, 0x58DB, 0x3799, 0x60A0, 0x2750, 0x3759, 0x8953, 0x7122, 0x81F9, 0x5524, 0x8971, 0x3A1D] v46 = Int('v46') v47 = Int('v47') v48 = Int('v48') v49 = Int('v49') v50 = Int('v50') v51 = Int('v51') v52 = Int('v52') v53 = Int('v53') v54 = Int('v54') v55 = Int('v55') v56 = Int('v56') v57 = Int('v57') v58 = Int('v58') v59 = Int('v59') v60 = Int('v60') v61 = Int('v61') v62 = Int('v62') v63 = Int('v63') v64 = Int('v64') v65 = Int('v65') v66 = Int('v66') v67 = Int('v67') v68 = Int('v68') v69 = Int('v69') v70 = Int('v70') v71 = Int('v71') v72 = Int('v72') v73 = Int('v73') v74 = Int('v74') v75 = Int('v75') v76 = Int('v76') v77 = Int('v77') v78 = Int('v78') v79 = Int('v79') v80 = Int('v80') v81 = Int('v81') v82 = Int('v82') v83 = Int('v83') v84 = Int('v84') v85 = Int('v85') v86 = Int('v86') v87 = Int('v87') s = Solver() s.add(res[0] == 34 * v49 + 12 * v46 + 53 * v47 + 6 * v48 + 58 * v50 + 36 * v51 + v52) s.add(res[1] == 27 * v50 + 73 * v49 + 12 * v48 + 83 * v46 + 85 * v47 + 96 * v51 + 52 * v52) s.add(res[2] == 24 * v48 + 78 * v46 + 53 * v47 + 36 * v49 + 86 * v50 + 25 * v51 + 46 * v52) s.add(res[3] == 78 * v47 + 39 * v46 + 52 * v48 + 9 * v49 + 62 * v50 + 37 * v51 + 84 * v52) s.add(res[4] == 48 * v50 + 14 * v48 + 23 * v46 + 6 * v47 + 74 * v49 + 12 * v51 + 83 * v52) s.add(res[5] == 15 * v51 + 48 * v50 + 92 * v48 + 85 * v47 + 27 * v46 + 42 * v49 + 72 * v52) s.add(res[6] == 26 * v51 + 67 * v49 + 6 * v47 + 4 * v46 + 3 * v48 + 68 * v52) s.add(res[7] == 34 * v56 + 12 * v53 + 53 * v54 + 6 * v55 + 58 * v57 + 36 * v58 + v59) s.add(res[8] == 27 * v57 + 73 * v56 + 12 * v55 + 83 * v53 + 85 * v54 + 96 * v58 + 52 * v59) s.add(res[9] == 24 * v55 + 78 * v53 + 53 * v54 + 36 * v56 + 86 * v57 + 25 * v58 + 46 * v59) s.add(res[10] == 78 * v54 + 39 * v53 + 52 * v55 + 9 * v56 + 62 * v57 + 37 * v58 + 84 * v59) s.add(res[11] == 48 * v57 + 14 * v55 + 23 * v53 + 6 * v54 + 74 * v56 + 12 * v58 + 83 * v59) s.add(res[12] == 15 * v58 + 48 * v57 + 92 * v55 + 85 * v54 + 27 * v53 + 42 * v56 + 72 * v59) s.add(res[13] == 26 * v58 + 67 * v56 + 6 * v54 + 4 * v53 + 3 * v55 + 68 * v59) s.add(res[14] == 34 * v63 + 12 * v60 + 53 * v61 + 6 * v62 + 58 * v64 + 36 * v65 + v66) s.add(res[15] == 27 * v64 + 73 * v63 + 12 * v62 + 83 * v60 + 85 * v61 + 96 * v65 + 52 * v66) s.add(res[16] == 24 * v62 + 78 * v60 + 53 * v61 + 36 * v63 + 86 * v64 + 25 * v65 + 46 * v66) s.add(res[17] == 78 * v61 + 39 * v60 + 52 * v62 + 9 * v63 + 62 * v64 + 37 * v65 + 84 * v66) s.add(res[18] == 48 * v64 + 14 * v62 + 23 * v60 + 6 * v61 + 74 * v63 + 12 * v65 + 83 * v66) s.add(res[19] == 15 * v65 + 48 * v64 + 92 * v62 + 85 * v61 + 27 * v60 + 42 * v63 + 72 * v66) s.add(res[20] == 26 * v65 + 67 * v63 + 6 * v61 + 4 * v60 + 3 * v62 + 68 * v66) s.add(res[21] == 34 * v70 + 12 * v67 + 53 * v68 + 6 * v69 + 58 * v71 + 36 * v72 + v73) s.add(res[22] == 27 * v71 + 73 * v70 + 12 * v69 + 83 * v67 + 85 * v68 + 96 * v72 + 52 * v73) s.add(res[23] == 24 * v69 + 78 * v67 + 53 * v68 + 36 * v70 + 86 * v71 + 25 * v72 + 46 * v73) s.add(res[24] == 78 * v68 + 39 * v67 + 52 * v69 + 9 * v70 + 62 * v71 + 37 * v72 + 84 * v73) s.add(res[25] == 48 * v71 + 14 * v69 + 23 * v67 + 6 * v68 + 74 * v70 + 12 * v72 + 83 * v73) s.add(res[26] == 15 * v72 + 48 * v71 + 92 * v69 + 85 * v68 + 27 * v67 + 42 * v70 + 72 * v73) s.add(res[27] == 26 * v72 + 67 * v70 + 6 * v68 + 4 * v67 + 3 * v69 + 68 * v73) s.add(res[28] == 34 * v77 + 12 * v74 + 53 * v75 + 6 * v76 + 58 * v78 + 36 * v79 + v80) s.add(res[29] == 27 * v78 + 73 * v77 + 12 * v76 + 83 * v74 + 85 * v75 + 96 * v79 + 52 * v80) s.add(res[30] == 24 * v76 + 78 * v74 + 53 * v75 + 36 * v77 + 86 * v78 + 25 * v79 + 46 * v80) s.add(res[31] == 78 * v75 + 39 * v74 + 52 * v76 + 9 * v77 + 62 * v78 + 37 * v79 + 84 * v80) s.add(res[32] == 48 * v78 + 14 * v76 + 23 * v74 + 6 * v75 + 74 * v77 + 12 * v79 + 83 * v80) s.add(res[33] == 15 * v79 + 48 * v78 + 92 * v76 + 85 * v75 + 27 * v74 + 42 * v77 + 72 * v80) s.add(res[34] == 26 * v79 + 67 * v77 + 6 * v75 + 4 * v74 + 3 * v76 + 68 * v80) s.add(res[35] == 34 * v84 + 12 * v81 + 53 * v82 + 6 * v83 + 58 * v85 + 36 * v86 + v87) s.add(res[36] == 27 * v85 + 73 * v84 + 12 * v83 + 83 * v81 + 85 * v82 + 96 * v86 + 52 * v87) s.add(res[37] == 24 * v83 + 78 * v81 + 53 * v82 + 36 * v84 + 86 * v85 + 25 * v86 + 46 * v87) s.add(res[38] == 78 * v82 + 39 * v81 + 52 * v83 + 9 * v84 + 62 * v85 + 37 * v86 + 84 * v87) s.add(res[39] == 48 * v85 + 14 * v83 + 23 * v81 + 6 * v82 + 74 * v84 + 12 * v86 + 83 * v87) s.add(res[40] == 15 * v86 + 48 * v85 + 92 * v83 + 85 * v82 + 27 * v81 + 42 * v84 + 72 * v87) s.add(res[41] == 26 * v86 + 67 * v84 + 6 * v82 + 4 * v81 + 3 * v83 + 68 * v87) print(s.check()) m = s.model() for d in m.decls(): print("'%s': %s," % (d.name(), m[d])) res = {'v84': 54, 'v65': 52, 'v63': 57, 'v74': 45, 'v47': 108, 'v62': 98, 'v81': 97, 'v64': 45, 'v48': 97, 'v51': 55, 'v58': 51, 'v53': 49, 'v49': 103, 'v55': 49, 'v57': 52, 'v67': 49, 'v54': 55, 'v70': 57, 'v69': 45, 'v56': 100, 'v86': 56, 'v72': 48, 'v60': 54, 'v78': 52, 'v68': 56, 'v79': 99, 'v75': 54, 'v46': 102, 'v77': 49, 'v76': 101, 'v50': 123, 'v61': 51, 'v71': 57, 'v82': 102, 'v83': 101, 'v85': 52, 'v87': 125, 'v80': 50, 'v73': 101, 'v66': 101, 'v59': 45, 'v52': 101, } for i in sorted(res): print(chr(res[i]), end="")
|