tuctf-grammarless-z3.py

#!/usr/bin/env python

# checkkey(S,R) :- lt_paren(S,S1), key(S1,S2,V1), rt_paren(S2,R), V1 is 82944.
# key(S,R,V) :- oct(S,S1,V1), amper(S1,S2), oct(S2,R,V2), V is V1 * V2.
# oct(S,R,V) :- quad(S,S1,V1), hyphen(S1,S2), quad(S2,R,V2), V is V1 + V2.
# quad(S,R,V) :- pair(S,S1,V1), comma(S1,S2), pair(S2,R,V2), V is V1* V2.
# pair(S,R,V) :- digit(S,S1,V1), digit(S1,R,V2), V is V1 + V2.

# nc grammarlesson.tuctf.com 6661
# (96,57-57,72&35,53-79,77)

# { key }
# { oct & oct }
# { quad - quad & oct - oct }
# { pair,pair - pair,pair & pair,pair - pair,pair }

from z3 import *
import string

def addvar(n):
  globals()[n] = BitVec(n,32);

solver = z3.Solver()
addvar("oct1")
addvar("oct2")
solver.add(oct1 * oct2 == BitVecVal(82944,32))
addvar("quad1")
addvar("quad2")
solver.add(quad1 + quad2 == oct1)
addvar("quad3")
addvar("quad4")
solver.add(quad3 + quad4 == oct2)
addvar("pair1")
addvar("pair2")
solver.add(pair1 * pair2 == quad1)
addvar("pair3")
addvar("pair4")
solver.add(pair3 * pair4 == quad2)
addvar("pair5")
addvar("pair6")
solver.add(pair5 * pair6 == quad3)
addvar("pair7")
addvar("pair8")
solver.add(pair7 * pair8 == quad4)
addvar("digit1")
addvar("digit2")
solver.add(digit1 + digit2 == pair1)
addvar("digit3")
addvar("digit4")
solver.add(digit3 + digit4 == pair2)
addvar("digit5")
addvar("digit6")
solver.add(digit5 + digit6 == pair3)
addvar("digit7")
addvar("digit8")
solver.add(digit7 + digit8 == pair4)
addvar("digit9")
addvar("digit10")
solver.add(digit9 + digit10 == pair5)
addvar("digit11")
addvar("digit12")
solver.add(digit11 + digit12 == pair6)
addvar("digit13")
addvar("digit14")
solver.add(digit13 + digit14 == pair7)
addvar("digit15")
addvar("digit16")
solver.add(digit15 + digit16 == pair8)

for i in range(1,17):
  solver.add(globals()["digit%i" % i] >= BitVecVal(0,32))
  solver.add(globals()["digit%i" % i] <= BitVecVal(9,32))

print solver.check()
s = solver.model()

# (96,57-57,72&35,53-79,77)
# (57,96-57,72&35,53-79,77)
# (75,96-57,72&35,53-79,77)
# (75,69-57,72&35,53-79,77)
# (57,69-57,72&35,53-79,77)
# (57,69-57,72&35,53-97,77)
# (57,96-57,72&35,53-97,77)
# (57,96-75,72&35,53-97,77)
# (57,96-75,27&35,53-97,77)
# (57,96-75,27&35,35-97,77)
# Here, have a flag!
# TUCTF{Gr4mm3r_1s_v3ry_imp0rtAnT!_4ls0_Pr0log_iz_c00l!}


print s

# print solver.check()
# n = solver.model()
# print n
import sys
sys.exit()
soln_array = {}
for d in n.decls():
  print "%s = %s" % (d.name(),n[d])
  soln_array[d.name()] = n[d]

out = ""
for i in range(0,25):
  vn = check(i)
  out += chr(int(str(soln_array[vn])))

print out