z3::solver

# Install
pip install z3-solver

# Import
from z3 import *

# Core workflow:
# 1. Declare variables (unknowns)
# 2. Add constraints (what we know)
# 3. solve() → get values satisfying constraints

s = Solver()
x = Int('x')
s.add(x > 0, x < 100, x * 3 == 42)
if s.check() == sat:
    print(s.model()[x])   # → 14

# Solver states
s.check()   # → sat (solution exists)
            # → unsat (no solution)
            # → unknown (timeout)

s.model()   # get solution (only after sat)
s.push()    # save checkpoint
s.pop()     # restore checkpoint
s.reset()   # clear all constraints
s.assertions()  # list all added constraints

# Print full model
m = s.model()
for d in m.decls():
    print(d.name(), '=', m[d])

# Integer (unbounded)
x = Int('x')
a, b, c = Ints('a b c')

# Real number
r = Real('r')

# Boolean
p = Bool('p')
p, q = Bools('p q')

# Bit-vector (most useful for CTF!)
x = BitVec('x', 32)          # 32-bit
x = BitVec('x', 8)           # byte
x = BitVec('x', 64)          # 64-bit
xs = BitVecs('x0 x1 x2 x3', 8) # four bytes

# Array of bit-vectors (e.g. flag bytes)
flag = [BitVec(f'c{i}', 8) for i in range(32)]

# Get integer value
m = s.model()
val = m[x].as_long()          # Int/BitVec → Python int
val = m.eval(x).as_long()     # evaluate expression

# Get flag as string
flag = [BitVec(f'c{i}', 8) for i in range(20)]
# ... add constraints ...
if s.check() == sat:
    m = s.model()
    result = bytes([m[flag[i]].as_long() for i in range(20)])
    print(result.decode())

# Handle None (unconstrained variable)
v = m[x]
if v is not None:
    print(v.as_long())
else:
    print('unconstrained — any value works')

# Standard arithmetic (works on Int and BitVec)
s.add(x + y == 42)
s.add(x - y > 0)
s.add(x * 3 == 99)
s.add(x / 4 == 10)       # integer division
s.add(x % 7 == 3)        # modulo

# Comparison
s.add(x == 42)
s.add(x != 0)
s.add(x >= 32, x <= 126)  # printable ASCII range

# Boolean logic
s.add(And(x > 0, y > 0))
s.add(Or(x == 1, x == 2))
s.add(Not(x == 0))
s.add(Implies(x > 10, y > 10))
s.add(If(x > 0, x, -x) == 5)   # ternary / abs

# XOR (BitVec only)
s.add(x ^ 0x42 == 0x7f)

# Bitwise (use BitVec, not Int)
s.add(x & 0xff == 0x41)       # AND
s.add(x | 0x20 == 0x61)       # OR
s.add(x ^ 0x13 == 0x72)       # XOR
s.add(~x == 0xffffffbe)       # NOT
s.add(x << 2 == 0x40)         # left shift
s.add(LShR(x, 1) == 0x20)     # logical right shift
s.add(x >> 1 == 0x20)         # arithmetic right shift

# Rotation (no native → implement manually)
def RotL(x, n, bits=32):
    return (x << n) | LShR(x, bits - n)
def RotR(x, n, bits=32):
    return LShR(x, n) | (x << (bits - n))

# Signed vs unsigned comparison
s.add(ULT(x, 256))            # unsigned less-than
s.add(UGT(x, 0))              # unsigned greater-than

from z3 import *

# Binary does: key[0]*31 + key[1]*17 == 0x1337
#              key[0] ^ key[1] == 0x55
#              all bytes printable

s = Solver()
key = [BitVec(f'k{i}', 8) for i in range(8)]

# Printable constraint on all bytes
for k in key:
    s.add(k >= 0x20, k <= 0x7e)

# Business logic constraints (from reverse engineering)
s.add(ZeroExt(8, key[0]) * 31 + ZeroExt(8, key[1]) * 17 == 0x1337)
s.add(key[0] ^ key[1] == 0x55)

if s.check() == sat:
    m = s.model()
    result = bytes([m[key[i]].as_long() for i in range(8)])
    print('Key:', result)

from z3 import *

# Binary: encrypted = [x ^ (i * 3 + 7) for i, x in enumerate(flag)]
# We have encrypted output, want original flag

encrypted = [0x72, 0x64, 0x71, 0x77, 0x7e, 0x68, 0x57, 0x74, 0x41, 0x6f]

s = Solver()
flag = [BitVec(f'f{i}', 8) for i in range(len(encrypted))]

for i, (f, enc) in enumerate(zip(flag, encrypted)):
    s.add(f >= 0x20, f <= 0x7e)              # printable
    key_byte = BitVecVal((i * 3 + 7) & 0xff, 8)
    s.add(f ^ key_byte == enc)               # encryption constraint

if s.check() == sat:
    m = s.model()
    print(bytes([m[flag[i]].as_long() for i in range(len(encrypted))]).decode())

from z3 import *

# General pattern: grid of constrained integers
cells = [[Int(f'c{r}{c}') for c in range(9)] for r in range(9)]
s = Solver()

# Each cell 1-9
for row in cells:
    for cell in row:
        s.add(cell >= 1, cell <= 9)

# Each row has distinct values
for row in cells:
    s.add(Distinct(*row))

# Each column has distinct values
for col in range(9):
    s.add(Distinct(*[cells[r][col] for r in range(9)]))

# Givens
given = [(0,0,5), (0,1,3), (1,6,6)]  # (row, col, value)
for r, c, v in given:
    s.add(cells[r][c] == v)

from z3 import *

# Custom hash: h = sum(ord(c) * (i+1) for i,c in enumerate(flag))
# We know h = 0x1337, length = 8

s = Solver()
flag = [BitVec(f'c{i}', 32) for i in range(8)]

# Printable ASCII
for c in flag:
    s.add(c >= 0x20, c <= 0x7e)

# Hash constraint
h = BitVecVal(0, 32)
for i, c in enumerate(flag):
    h = h + c * (i + 1)
s.add(h == 0x1337)

# Known prefix
s.add(flag[0] == ord('p'))
s.add(flag[1] == ord('i'))

from z3 import *

# Extract bits [high:low] from bitvec
x = BitVec('x', 32)
hi_byte = Extract(31, 24, x)    # top byte
lo_byte = Extract(7,  0,  x)    # bottom byte
nibble  = Extract(7,  4,  x)    # high nibble of byte

# Concatenate bit-vectors
a = BitVec('a', 8)
b = BitVec('b', 8)
ab = Concat(a, b)               # 16-bit: a in high bits
s.add(ab == 0x4142)             # a='A', b='B'

# Zero-extend (widen without sign)
x8  = BitVec('x', 8)
x32 = ZeroExt(24, x8)          # 8→32 bits
x32 = SignExt(24, x8)          # sign-extend

# Truncate
x32 = BitVec('x', 32)
x8  = Extract(7, 0, x32)       # low 8 bits

from z3 import *

# Flag as array of bytes — most common CTF pattern
n = 16  # flag length
flag = [BitVec(f'c{i}', 8) for i in range(n)]

s = Solver()

# Constrain to printable
for c in flag:
    s.add(c >= 32, c <= 126)

# Known prefix: picoCTF{
prefix = b'picoCTF{'
for i, b in enumerate(prefix):
    s.add(flag[i] == b)

# Known suffix: }
s.add(flag[-1] == ord('}'))

# Add reversed-engineered constraints here
# e.g. from decompiled check function

if s.check() == sat:
    m = s.model()
    print(bytes([m[flag[i]].as_long() for i in range(n)]).decode())

from z3 import *

s = Solver()
x = BitVec('x', 8)
s.add(x > 10, x < 20)

# Enumerate all solutions
solutions = []
while s.check() == sat:
    m = s.model()
    val = m[x].as_long()
    solutions.append(val)
    s.add(x != val)             # block this solution

print(solutions)                # [11, 12, 13, 14, 15, 16, 17, 18, 19]

from z3 import *

# Optimizer: find min/max of expression
opt = Optimize()
x = Int('x')
opt.add(x > 0, x < 1000)
opt.add(x * x - 10 * x == 0)

opt.minimize(x)
if opt.check() == sat:
    print('min x:', opt.model()[x])

opt2 = Optimize()
opt2.add(x > 0, x < 1000)
opt2.maximize(x)
if opt2.check() == sat:
    print('max x:', opt2.model()[x])