-
Notifications
You must be signed in to change notification settings - Fork 65
/
theorem_prover.py
47 lines (41 loc) · 1.11 KB
/
theorem_prover.py
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
import random
target = 114514
challenges = 32
def get_value(expr):
for char in expr:
if char not in "()+-*/%~&|^" + str(target):
return False
if "".join([char for char in expr if char in str(target)]) != str(target):
return False
if "**" in expr or "//" in expr or "()" in expr:
return False
expr = expr.replace("/", "//")
try:
v = eval(expr)
assert type(v) == type(0)
except:
return False
else:
return v
for i in range(challenges):
n = random.randint(1, min(target, 10**i))
expr = input(("Challenge ({}/{}): {} = ".format(i + 1, challenges, n))).strip()
if len(expr) > 256:
print("Too long!")
print("Failed!")
break
v = get_value(expr)
if v is False:
print("Invalid expr!")
print("Failed!")
break
else:
if v == n:
print("Q.E.D.")
else:
print("{} = {} (which is not {})".format(expr, v, n))
print("Failed!")
break
else:
print("You finished all challenges!")
print(open("flag").read())