From 13dfd186294926ef4588632f5fdac8a875c8e469 Mon Sep 17 00:00:00 2001
From: Mingliang Zeng <zengmingliang1998@gmail.com>
Date: Fri, 6 Nov 2020 20:43:14 +0800
Subject: [PATCH] theorem prover src

---
 official/超精巧的数字论证器/src/Dockerfile    |  3 ++
 .../超精巧的数字论证器/src/theorem_prover.py  | 47 +++++++++++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 official/超精巧的数字论证器/src/Dockerfile
 create mode 100644 official/超精巧的数字论证器/src/theorem_prover.py

diff --git a/official/超精巧的数字论证器/src/Dockerfile b/official/超精巧的数字论证器/src/Dockerfile
new file mode 100644
index 0000000..7940ada
--- /dev/null
+++ b/official/超精巧的数字论证器/src/Dockerfile
@@ -0,0 +1,3 @@
+FROM python:3.8
+COPY theorem_prover.py /
+CMD ["/usr/local/bin/python3", "-u", "/theorem_prover.py"]
diff --git a/official/超精巧的数字论证器/src/theorem_prover.py b/official/超精巧的数字论证器/src/theorem_prover.py
new file mode 100644
index 0000000..6ee7e8d
--- /dev/null
+++ b/official/超精巧的数字论证器/src/theorem_prover.py
@@ -0,0 +1,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())