Fix file loading issues
Browse files- backend/app.py +4 -1
- backend/solver.py +7 -5
backend/app.py
CHANGED
@@ -9,6 +9,9 @@ BASE_DIR = os.path.dirname(os.path.abspath(__file__))
|
|
9 |
example_path = os.path.join(BASE_DIR, "Example.txt")
|
10 |
with open(example_path, "r", encoding="utf-8") as f:
|
11 |
DEFAULT_SYS_CONTENT = f.read()
|
|
|
|
|
|
|
12 |
|
13 |
# Only initialize once
|
14 |
app = Flask(__name__, static_folder='static', static_url_path='')
|
@@ -49,7 +52,7 @@ def solve():
|
|
49 |
if puzzle_index is None or puzzle_text is None or expected_solution is None:
|
50 |
return jsonify({"success": False, "error": "Missing puzzle data"}), 400
|
51 |
|
52 |
-
result = solve_puzzle(puzzle_index, puzzle_text, expected_solution, sys_content)
|
53 |
return jsonify({"success": True, "result": result})
|
54 |
|
55 |
@app.route("/default_sys_content", methods=["GET"])
|
|
|
9 |
example_path = os.path.join(BASE_DIR, "Example.txt")
|
10 |
with open(example_path, "r", encoding="utf-8") as f:
|
11 |
DEFAULT_SYS_CONTENT = f.read()
|
12 |
+
sat_cnt_path = os.path.join(BASE_DIR, "Sat_cnt.txt")
|
13 |
+
with open(sat_cnt_path, "r", encoding="utf-8") as f:
|
14 |
+
SAT_CNT_CONTENT = f.read()
|
15 |
|
16 |
# Only initialize once
|
17 |
app = Flask(__name__, static_folder='static', static_url_path='')
|
|
|
52 |
if puzzle_index is None or puzzle_text is None or expected_solution is None:
|
53 |
return jsonify({"success": False, "error": "Missing puzzle data"}), 400
|
54 |
|
55 |
+
result = solve_puzzle(puzzle_index, puzzle_text, expected_solution, sys_content, SAT_CNT_CONTENT)
|
56 |
return jsonify({"success": True, "result": result})
|
57 |
|
58 |
@app.route("/default_sys_content", methods=["GET"])
|
backend/solver.py
CHANGED
@@ -8,7 +8,7 @@ from deep_convert import deep_convert
|
|
8 |
from openai import OpenAI
|
9 |
from dotenv import load_dotenv
|
10 |
|
11 |
-
def solve_puzzle(index, puzzle, expected_solution, sys_content):
|
12 |
"""
|
13 |
使用 sys_content + puzzle 调用模型,生成 Z3 Python 代码,
|
14 |
运行并比对输出是否与 expected_solution 相同。
|
@@ -146,14 +146,16 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
|
|
146 |
if satisfied(constraint) == "unsat":
|
147 |
problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
|
148 |
|
149 |
-
with open("Sat_cnt.txt", "r") as f:
|
150 |
-
|
|
|
|
|
151 |
cnt_cons = 0
|
152 |
problematic_constraints += "\nMultiple solutions judge:\n"
|
153 |
code_by_line_experiment = code_to_run.split("\n")[:last_cons_line + 1]
|
154 |
code_by_line_experiment.append("\n")
|
155 |
def run_result():
|
156 |
-
experiment_code = "\n".join(code_by_line_experiment) +
|
157 |
sat_checker = experiment_code.strip()
|
158 |
result = subprocess.run(
|
159 |
[sys.executable, "-c", sat_checker],
|
@@ -163,7 +165,7 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content):
|
|
163 |
)
|
164 |
return result.stdout.strip()
|
165 |
res = run_result()
|
166 |
-
# print("\n".join(code_by_line_experiment) +
|
167 |
# print(res)
|
168 |
if not res or res == "error":
|
169 |
problematic_constraints += "Unable to judge."
|
|
|
8 |
from openai import OpenAI
|
9 |
from dotenv import load_dotenv
|
10 |
|
11 |
+
def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content):
|
12 |
"""
|
13 |
使用 sys_content + puzzle 调用模型,生成 Z3 Python 代码,
|
14 |
运行并比对输出是否与 expected_solution 相同。
|
|
|
146 |
if satisfied(constraint) == "unsat":
|
147 |
problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
|
148 |
|
149 |
+
# with open("Sat_cnt.txt", "r") as f:
|
150 |
+
# sat_cnt = f.read()
|
151 |
+
# Cannot directly load because the server strucutre
|
152 |
+
|
153 |
cnt_cons = 0
|
154 |
problematic_constraints += "\nMultiple solutions judge:\n"
|
155 |
code_by_line_experiment = code_to_run.split("\n")[:last_cons_line + 1]
|
156 |
code_by_line_experiment.append("\n")
|
157 |
def run_result():
|
158 |
+
experiment_code = "\n".join(code_by_line_experiment) + sat_cnt_content
|
159 |
sat_checker = experiment_code.strip()
|
160 |
result = subprocess.run(
|
161 |
[sys.executable, "-c", sat_checker],
|
|
|
165 |
)
|
166 |
return result.stdout.strip()
|
167 |
res = run_result()
|
168 |
+
# print("\n".join(code_by_line_experiment) + sat_cnt_content)
|
169 |
# print(res)
|
170 |
if not res or res == "error":
|
171 |
problematic_constraints += "Unable to judge."
|