#!/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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment