import re
from z3 import *

# ==============================================================================
# 1. RAW DATA (The C++ code you provided)
# ==============================================================================
raw_cpp_code = """
  *((_DWORD *)this + 15) = 1;
  *((_DWORD *)this + 16) = 2;
  *((_DWORD *)this + 25) = 2;
  *((_DWORD *)this + 26) = 4;
  *((_DWORD *)this + 27) = 5;
  *((_DWORD *)this + 28) = 3;
  *((_DWORD *)this + 30) = 6;
  *((_DWORD *)this + 31) = 3;
  *((_DWORD *)this + 32) = 3;
  *((_DWORD *)this + 34) = 4;
  *((_DWORD *)this + 37) = 6;
  *((_DWORD *)this + 43) = 4;
  *((_DWORD *)this + 44) = 5;
  *((_DWORD *)this + 46) = 5;
  *((_DWORD *)this + 47) = 6;
  *((_DWORD *)this + 53) = 5;
  *((_DWORD *)this + 56) = 7;
  *((_DWORD *)this + 65) = 10;
  *((_DWORD *)this + 66) = 10;
  *((_DWORD *)this + 67) = 7;
  *((_DWORD *)this + 68) = 8;
  *((_DWORD *)this + 70) = 4;
  *((_DWORD *)this + 71) = 11;
  *((_DWORD *)this + 72) = 9;
  *((_DWORD *)this + 77) = 11;
  *((_DWORD *)this + 81) = 10;
  *((_DWORD *)this + 90) = 6;
  *((_DWORD *)this + 91) = 12;
  *((_DWORD *)this + 92) = 11;
  *((_DWORD *)this + 94) = 12;
  *((_DWORD *)this + 101) = 11;
  *((_DWORD *)this + 103) = 13;
  *((_DWORD *)this + 112) = 16;
  *((_DWORD *)this + 113) = 14;
  *((_DWORD *)this + 122) = 15;
  *((_DWORD *)this + 131) = 16;
  *((_DWORD *)this + 140) = 17;
  *((_DWORD *)this + 142) = 19;
  *((_DWORD *)this + 143) = 19;
  *((_DWORD *)this + 144) = 18;
  *((_DWORD *)this + 149) = 13;
  *((_DWORD *)this + 153) = 21;
  *((_DWORD *)this + 154) = 21;
  *((_DWORD *)this + 155) = 19;
  *((_DWORD *)this + 164) = 20;
  *((_DWORD *)this + 166) = 21;
  *((_DWORD *)this + 173) = 22;
  *((_DWORD *)this + 175) = 21;
  *((_DWORD *)this + 176) = 21;
  *((_DWORD *)this + 177) = 17;
  *((_DWORD *)this + 178) = 21;
  *((_DWORD *)this + 179) = 22;
  *((_DWORD *)this + 188) = 23;
  *((_DWORD *)this + 190) = 25;
  *((_DWORD *)this + 191) = 24;
  *((_DWORD *)this + 197) = 25;
  *((_DWORD *)this + 200) = 25;
  *((_DWORD *)this + 209) = 26;
  *((_DWORD *)this + 218) = 28;
  *((_DWORD *)this + 219) = 27;
  *((_DWORD *)this + 228) = 28;
  *((_DWORD *)this + 230) = 29;
  *((_DWORD *)this + 237) = 28;
  *((_DWORD *)this + 239) = 30;
  *((_DWORD *)this + 248) = 26;
  *((_DWORD *)this + 249) = 30;
  *((_DWORD *)this + 250) = 26;
  *((_DWORD *)this + 251) = 31;
  *((_DWORD *)this + 260) = 32;
  *((_DWORD *)this + 262) = 33;
  *((_DWORD *)this + 269) = 32;
  *((_DWORD *)this + 271) = 35;
  *((_DWORD *)this + 272) = 34;
  *((_DWORD *)this + 281) = 36;
  *((_DWORD *)this + 282) = 37;
  *((_DWORD *)this + 283) = 35;
  *((_DWORD *)this + 292) = 36;
  *((_DWORD *)this + 294) = 37;
  *((_DWORD *)this + 301) = 36;
  *((_DWORD *)this + 303) = 38;
  *((_DWORD *)this + 312) = 39;
  *((_DWORD *)this + 321) = 40;
  *((_DWORD *)this + 330) = 41;
  *((_DWORD *)this + 339) = 41;
  *((_DWORD *)this + 340) = 42;
  *((_DWORD *)this + 342) = 43;
  *((_DWORD *)this + 349) = 45;
  *((_DWORD *)this + 351) = 45;
  *((_DWORD *)this + 352) = 43;
  *((_DWORD *)this + 353) = 46;
  *((_DWORD *)this + 354) = 43;
  *((_DWORD *)this + 355) = 44;
  *((_DWORD *)this + 364) = 45;
  *((_DWORD *)this + 366) = 47;
  *((_DWORD *)this + 367) = 41;
  *((_DWORD *)this + 368) = 46;
  *((_DWORD *)this + 373) = 41;
  *((_DWORD *)this + 377) = 47;
  *((_DWORD *)this + 386) = 49;
  *((_DWORD *)this + 387) = 48;
  *((_DWORD *)this + 396) = 49;
  *((_DWORD *)this + 398) = 50;
  *((_DWORD *)this + 405) = 52;
  *((_DWORD *)this + 407) = 51;
  *((_DWORD *)this + 416) = 52;
  *((_DWORD *)this + 425) = 53;
  *((_DWORD *)this + 434) = 55;
  *((_DWORD *)this + 435) = 54;
  *((_DWORD *)this + 444) = 55;
  *((_DWORD *)this + 446) = 58;
  *((_DWORD *)this + 447) = 56;
  *((_DWORD *)this + 453) = 57;
  *((_DWORD *)this + 456) = 57;
  *((_DWORD *)this + 465) = 58;
  *((_DWORD *)this + 474) = 60;
  *((_DWORD *)this + 475) = 59;
  *((_DWORD *)this + 484) = 60;
  *((_DWORD *)this + 486) = 61;
  *((_DWORD *)this + 493) = 60;
  *((_DWORD *)this + 495) = 62;
  *((_DWORD *)this + 504) = 63;
  *((_DWORD *)this + 513) = 66;
  *((_DWORD *)this + 514) = 66;
  *((_DWORD *)this + 515) = 64;
  *((_DWORD *)this + 524) = 65;
  *((_DWORD *)this + 526) = 66;
  *((_DWORD *)this + 533) = 68;
  *((_DWORD *)this + 535) = 67;
  *((_DWORD *)this + 544) = 68;
  *((_DWORD *)this + 553) = 69;
  *((_DWORD *)this + 562) = 70;
  *((_DWORD *)this + 571) = 66;
  *((_DWORD *)this + 572) = 71;
  *((_DWORD *)this + 574) = 73;
  *((_DWORD *)this + 575) = 74;
  *((_DWORD *)this + 576) = 72;
  *((_DWORD *)this + 581) = 67;
  *((_DWORD *)this + 585) = 74;
  *((_DWORD *)this + 586) = 73;
  *((_DWORD *)this + 595) = 74;
  *((_DWORD *)this + 604) = 75;
  *((_DWORD *)this + 606) = 76;
  *((_DWORD *)this + 613) = 75;
  *((_DWORD *)this + 615) = 77;
  *((_DWORD *)this + 624) = 78;
  *((_DWORD *)this + 633) = 79;
  *((_DWORD *)this + 642) = 82;
  *((_DWORD *)this + 643) = 80;
  *((_DWORD *)this + 652) = 81;
  *((_DWORD *)this + 654) = 82;
  *((_DWORD *)this + 661) = 81;
  *((_DWORD *)this + 663) = 83;
  *((_DWORD *)this + 672) = 84;
  *((_DWORD *)this + 681) = 85;
  *((_DWORD *)this + 690) = 86;
  *((_DWORD *)this + 699) = 88;
  *((_DWORD *)this + 700) = 87;
  *((_DWORD *)this + 702) = 89;
  *((_DWORD *)this + 703) = 87;
  *((_DWORD *)this + 704) = 88;
  *((_DWORD *)this + 709) = 83;
  *((_DWORD *)this + 713) = 91;
  *((_DWORD *)this + 714) = 89;
  *((_DWORD *)this + 723) = 90;
  *((_DWORD *)this + 732) = 91;
  *((_DWORD *)this + 734) = 94;
  *((_DWORD *)this + 735) = 87;
  *((_DWORD *)this + 736) = 87;
  *((_DWORD *)this + 737) = 92;
  *((_DWORD *)this + 741) = 93;
  *((_DWORD *)this + 746) = 88;
  *((_DWORD *)this + 747) = 93;
  *((_DWORD *)this + 756) = 94;
  *((_DWORD *)this + 758) = 95;
  *((_DWORD *)this + 765) = 97;
  *((_DWORD *)this + 767) = 97;
  *((_DWORD *)this + 768) = 96;
  *((_DWORD *)this + 777) = 99;
  *((_DWORD *)this + 778) = 99;
  *((_DWORD *)this + 779) = 97;
  *((_DWORD *)this + 788) = 98;
  *((_DWORD *)this + 790) = 99;
  *((_DWORD *)this + 797) = 100;
  *((_DWORD *)this + 799) = 100;
  *((_DWORD *)this + 808) = 101;
  *((_DWORD *)this + 817) = 102;
  *((_DWORD *)this + 826) = 103;
  *((_DWORD *)this + 835) = 99;
  *((_DWORD *)this + 836) = 104;
  *((_DWORD *)this + 838) = 106;
  *((_DWORD *)this + 839) = 105;
  *((_DWORD *)this + 845) = 100;
  *((_DWORD *)this + 848) = 108;
  *((_DWORD *)this + 849) = 108;
  *((_DWORD *)this + 850) = 101;
  *((_DWORD *)this + 851) = 106;
  *((_DWORD *)this + 860) = 107;
  *((_DWORD *)this + 862) = 108;
  *((_DWORD *)this + 869) = 107;
  *((_DWORD *)this + 871) = 109;
  *((_DWORD *)this + 880) = 109;
  *((_DWORD *)this + 881) = 109;
  *((_DWORD *)this + 882) = 110;
  *((_DWORD *)this + 891) = 111;
  *((_DWORD *)this + 894) = 107;
  *((_DWORD *)this + 895) = 111;
  *((_DWORD *)this + 896) = 112;
  *((_DWORD *)this + 900) = 114;
  *((_DWORD *)this + 901) = 114;
  *((_DWORD *)this + 905) = 108;
  *((_DWORD *)this + 906) = 113;
  *((_DWORD *)this + 915) = 114;
  *((_DWORD *)this + 918) = 116;
  *((_DWORD *)this + 919) = 114;
  *((_DWORD *)this + 920) = 115;
  *((_DWORD *)this + 924) = 110;
  *((_DWORD *)this + 925) = 110;
  *((_DWORD *)this + 929) = 115;
  *((_DWORD *)this + 930) = 116;
  *((_DWORD *)this + 939) = 117;
  *((_DWORD *)this + 948) = 118;
  *((_DWORD *)this + 950) = 119;
  *((_DWORD *)this + 957) = 120;
  *((_DWORD *)this + 959) = 120;
  *((_DWORD *)this + 968) = 121;
  *((_DWORD *)this + 977) = 122;
  *((_DWORD *)this + 986) = 123;
  *((_DWORD *)this + 995) = 125;
  *((_DWORD *)this + 996) = 124;
  *((_DWORD *)this + 998) = 125;
  *((_DWORD *)this + 1005) = 124;
  *((_DWORD *)this + 1007) = 126;
  *((_DWORD *)this + 1016) = 127;
  *((_DWORD *)this + 1025) = 128;
  *((_DWORD *)this + 1034) = 130;
  *((_DWORD *)this + 1035) = 129;
  *((_DWORD *)this + 1044) = 130;
  *((_DWORD *)this + 1046) = 133;
  *((_DWORD *)this + 1047) = 131;
  *((_DWORD *)this + 1053) = 126;
  *((_DWORD *)this + 1056) = 132;
  *((_DWORD *)this + 1065) = 128;
  *((_DWORD *)this + 1066) = 132;
  *((_DWORD *)this + 1067) = 133;
  *((_DWORD *)this + 1076) = 134;
  *((_DWORD *)this + 1078) = 135;
  *((_DWORD *)this + 1085) = 136;
  *((_DWORD *)this + 1087) = 136;
  *((_DWORD *)this + 1096) = 137;
  *((_DWORD *)this + 1105) = 138;
  *((_DWORD *)this + 1114) = 139;
  *((_DWORD *)this + 1123) = 142;
  *((_DWORD *)this + 1124) = 140;
  *((_DWORD *)this + 1126) = 142;
  *((_DWORD *)this + 1127) = 143;
  *((_DWORD *)this + 1128) = 141;
  *((_DWORD *)this + 1133) = 140;
  *((_DWORD *)this + 1137) = 144;
  *((_DWORD *)this + 1138) = 142;
  *((_DWORD *)this + 1147) = 143;
  *((_DWORD *)this + 1156) = 144;
  *((_DWORD *)this + 1158) = 147;
  *((_DWORD *)this + 1159) = 144;
  *((_DWORD *)this + 1160) = 146;
  *((_DWORD *)this + 1161) = 145;
  *((_DWORD *)this + 1165) = 146;
  *((_DWORD *)this + 1170) = 141;
  *((_DWORD *)this + 1171) = 146;
  *((_DWORD *)this + 1180) = 147;
  *((_DWORD *)this + 1182) = 148;
  *((_DWORD *)this + 1189) = 147;
  *((_DWORD *)this + 1191) = 148;
  *((_DWORD *)this + 1192) = 149;
  *((_DWORD *)this + 1201) = 151;
  *((_DWORD *)this + 1202) = 151;
  *((_DWORD *)this + 1203) = 150;
  *((_DWORD *)this + 1212) = 151;
  *((_DWORD *)this + 1214) = 152;
  *((_DWORD *)this + 1221) = 154;
  *((_DWORD *)this + 1223) = 153;
  *((_DWORD *)this + 1232) = 154;
  *((_DWORD *)this + 1241) = 155;
  *((_DWORD *)this + 1250) = 156;
  *((_DWORD *)this + 1259) = 156;
  *((_DWORD *)this + 1260) = 157;
  *((_DWORD *)this + 1262) = 157;
  *((_DWORD *)this + 1263) = 158;
  *((_DWORD *)this + 1269) = 160;
  *((_DWORD *)this + 1272) = 159;
  *((_DWORD *)this + 1281) = 159;
  *((_DWORD *)this + 1282) = 155;
  *((_DWORD *)this + 1283) = 160;
  *((_DWORD *)this + 1292) = 161;
  *((_DWORD *)this + 1294) = 164;
  *((_DWORD *)this + 1295) = 164;
  *((_DWORD *)this + 1296) = 162;
  *((_DWORD *)this + 1301) = 161;
  *((_DWORD *)this + 1305) = 163;
  *((_DWORD *)this + 1314) = 159;
  *((_DWORD *)this + 1315) = 164;
  *((_DWORD *)this + 1324) = 165;
  *((_DWORD *)this + 1326) = 167;
  *((_DWORD *)this + 1327) = 161;
  *((_DWORD *)this + 1328) = 166;
  *((_DWORD *)this + 1333) = 168;
  *((_DWORD *)this + 1337) = 169;
  *((_DWORD *)this + 1338) = 167;
  *((_DWORD *)this + 1347) = 168;
  *((_DWORD *)this + 1350) = 169;
  *((_DWORD *)this + 1356) = 171;
  *((_DWORD *)this + 1357) = 170;
  *((_DWORD *)this + 1359) = 170;
  *((_DWORD *)this + 1368) = 171;
  *((_DWORD *)this + 1377) = 167;
  *((_DWORD *)this + 1378) = 173;
  *((_DWORD *)this + 1379) = 172;
  *((_DWORD *)this + 1388) = 173;
  *((_DWORD *)this + 1390) = 174;
  *((_DWORD *)this + 1397) = 169;
  *((_DWORD *)this + 1399) = 170;
  *((_DWORD *)this + 1400) = 174;
  *((_DWORD *)this + 1401) = 177;
  *((_DWORD *)this + 1402) = 177;
  *((_DWORD *)this + 1403) = 175;
  *((_DWORD *)this + 1406) = 176;
  *((_DWORD *)this + 1412) = 175;
  *((_DWORD *)this + 1413) = 177;
  *((_DWORD *)this + 1415) = 176;
  *((_DWORD *)this + 1416) = 177;
  *((_DWORD *)this + 1425) = 178;
  *((_DWORD *)this + 1434) = 179;
  *((_DWORD *)this + 1443) = 180;
  *((_DWORD *)this + 1452) = 181;
  *((_DWORD *)this + 1461) = 184;
  *((_DWORD *)this + 1478) = 0;
  *((_DWORD *)this + 1479) = 23;
  *((_DWORD *)this + 1480) = 21;
  *((_DWORD *)this + 1481) = 32;
  *((_DWORD *)this + 1482) = 19;
  *((_DWORD *)this + 1483) = 17;
  *((_DWORD *)this + 1484) = 31;
  *((_DWORD *)this + 1485) = 38;
  *((_DWORD *)this + 1486) = 0;
"""

# ==============================================================================
# 2. PARSE DATA
# ==============================================================================
# We need to extract TransitionTable and TargetHistogram
# Transition table offset base = 6 (offset 24 bytes / 4)
# Target histogram offset base = 1479

TABLE_OFFSET_BASE = 6
HIST_OFFSET_BASE = 1479
NUM_HITS = 8

transition_table = {} # (state, hit) -> next_state
target_histogram = [0] * NUM_HITS

# Regex to find assignments: *((_DWORD *)this + OFFSET) = VALUE;
pattern = re.compile(r'\*\(\(_DWORD \*\)this \+ (\d+)\) = (\d+);')

print("[*] Parsing C++ code...")

matches = pattern.findall(raw_cpp_code)
for offset_str, value_str in matches:
    offset = int(offset_str)
    value = int(value_str)

    # Check if it belongs to Transition Table
    # The table is roughly between offset 6 and 1470
    if TABLE_OFFSET_BASE <= offset < 1478:
        # Calculate State and Hit
        # equation: offset = base + (state * 8) + hit
        local_off = offset - TABLE_OFFSET_BASE
        state = local_off // NUM_HITS
        hit = local_off % NUM_HITS
        transition_table[(state, hit)] = value
    
    # Check if it belongs to Target Histogram
    elif HIST_OFFSET_BASE <= offset < HIST_OFFSET_BASE + NUM_HITS:
        idx = offset - HIST_OFFSET_BASE
        target_histogram[idx] = value

print(f"[*] Parsed {len(transition_table)} transition rules.")
print(f"[*] Target Histogram: {target_histogram}")

# Calculate Flag Length from histogram
FLAG_LEN = sum(target_histogram)
print(f"[*] Calculated Flag Length: {FLAG_LEN}")

# The Success State is usually the state we reach after the last char.
# Based on the main(), it is 181.
SUCCESS_STATE = 181

# Initial state (offset +1478 = 0)
START_STATE = 0 
# Also, there is a distinct assignment `*v2 = 1`. v2 is offset 6. 
# offset 6 -> state 0, hit 0 -> next_state 1.
transition_table[(0, 0)] = 1

# ==============================================================================
# 3. Z3 SOLVER
# ==============================================================================
s = Solver()

# Variables: The sequence of hits (0-7)
hits = [Int(f'h_{i}') for i in range(FLAG_LEN)]
# Variables: The sequence of states
states = [Int(f's_{i}') for i in range(FLAG_LEN + 1)]

# 1. Domain Constraints
for h in hits:
    s.add(h >= 0, h < NUM_HITS)

# 2. Histogram Constraints
for k in range(NUM_HITS):
    s.add(Sum([If(h == k, 1, 0) for h in hits]) == target_histogram[k])

# 3. FSM Simulation
s.add(states[0] == START_STATE)

# We need to construct the lookup logic. 
# Since many transitions are missing (implied 0/fail), we only encode the valid ones.
# If a transition (state, hit) is NOT in our dictionary, it defaults to 0.

# Determine max state index to iterate safely
max_state = max([k[0] for k in transition_table.keys()] + [0])

print("[*] Building Z3 constraints (this might take a second)...")

for i in range(FLAG_LEN):
    curr_s = states[i]
    next_s = states[i+1]
    curr_h = hits[i]
    
    # Logic: next_s == Table[curr_s][curr_h]
    # We construct a big If-Else chain or rely on the fact that the path MUST exist.
    # Optimization: Only allow valid transitions found in the table.
    
    # Collect all valid transitions as a constraint:
    # Or( (curr_s == S1 And curr_h == H1 And next_s == S_next), ... )
    
    valid_transitions = []
    
    # We iterate through our known transitions
    for (t_state, t_hit), t_next in transition_table.items():
        valid_transitions.append(And(curr_s == t_state, curr_h == t_hit, next_s == t_next))
        
    # If the solver picks a state/hit combo not in our table, it goes to state 0
    # But since we demand the final state be 181, valid transitions must be taken.
    # So we simply enforce that one of the valid transitions MUST occur.
    s.add(Or(valid_transitions))

# 4. Success Condition
s.add(states[FLAG_LEN] == SUCCESS_STATE)

print("[*] Solving...")
if s.check() == sat:
    m = s.model()
    sol = "".join([str(m.evaluate(h).as_long()) for h in hits])
    print("\n[SUCCESS] Sequence Found:")
    print(sol)
else:
    print("\n[FAIL] UNSAT. No solution found.")