Test
Browse files
backend/__pycache__/solver.cpython-313.pyc
CHANGED
|
Binary files a/backend/__pycache__/solver.cpython-313.pyc and b/backend/__pycache__/solver.cpython-313.pyc differ
|
|
|
backend/solver.py
CHANGED
|
@@ -138,20 +138,24 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
|
|
| 138 |
problematic_constraints = "Issue: Wrong answer\n"
|
| 139 |
|
| 140 |
cnt_cons = 0
|
|
|
|
| 141 |
problematic_constraints += "\nSatisfaction judge:\n"
|
| 142 |
for i, line in enumerate(code_by_line):
|
| 143 |
if "s.add" in line and "pos" in line:
|
| 144 |
constraint = line.strip()
|
| 145 |
cnt_cons += 1
|
| 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 += "\
|
| 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():
|
|
@@ -168,16 +172,17 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
|
|
| 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."
|
| 172 |
else:
|
| 173 |
cur = int(res.split(':')[1])
|
|
|
|
| 174 |
for i, line in enumerate(code_by_line):
|
| 175 |
if "s.add" in line and "pos" in line:
|
| 176 |
cnt_cons += 1
|
| 177 |
code_by_line_experiment[i] = ""
|
| 178 |
res = run_result()
|
| 179 |
if not res or res == "error":
|
| 180 |
-
problematic_constraints += "Unable to judge."
|
| 181 |
break
|
| 182 |
now_cnt = int(res.split(':')[1])
|
| 183 |
if now_cnt == cur:
|
|
|
|
| 138 |
problematic_constraints = "Issue: Wrong answer\n"
|
| 139 |
|
| 140 |
cnt_cons = 0
|
| 141 |
+
ok_satisfied = True
|
| 142 |
problematic_constraints += "\nSatisfaction judge:\n"
|
| 143 |
for i, line in enumerate(code_by_line):
|
| 144 |
if "s.add" in line and "pos" in line:
|
| 145 |
constraint = line.strip()
|
| 146 |
cnt_cons += 1
|
| 147 |
if satisfied(constraint) == "unsat":
|
| 148 |
+
ok_satisfied = False
|
| 149 |
problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
|
| 150 |
+
if ok_satisfied:
|
| 151 |
+
problematic_constraints += "All constraints are satisfied.\n"
|
| 152 |
|
| 153 |
# with open("Sat_cnt.txt", "r") as f:
|
| 154 |
# sat_cnt = f.read()
|
| 155 |
# Cannot directly load because the server strucutre
|
| 156 |
|
| 157 |
cnt_cons = 0
|
| 158 |
+
problematic_constraints += "\nRedundency judge:\n"
|
| 159 |
code_by_line_experiment = code_to_run.split("\n")[:last_cons_line + 1]
|
| 160 |
code_by_line_experiment.append("\n")
|
| 161 |
def run_result():
|
|
|
|
| 172 |
# print("\n".join(code_by_line_experiment) + sat_cnt_content)
|
| 173 |
# print(res)
|
| 174 |
if not res or res == "error":
|
| 175 |
+
problematic_constraints += f"Unable to judge: {res}, {"\n".join(code_by_line_experiment) + sat_cnt_content}"
|
| 176 |
else:
|
| 177 |
cur = int(res.split(':')[1])
|
| 178 |
+
problematic_constraints += f"The number of solutions: {cur}\n"
|
| 179 |
for i, line in enumerate(code_by_line):
|
| 180 |
if "s.add" in line and "pos" in line:
|
| 181 |
cnt_cons += 1
|
| 182 |
code_by_line_experiment[i] = ""
|
| 183 |
res = run_result()
|
| 184 |
if not res or res == "error":
|
| 185 |
+
problematic_constraints += f"Unable to judge further: {res}, {"\n".join(code_by_line_experiment) + sat_cnt_content}"
|
| 186 |
break
|
| 187 |
now_cnt = int(res.split(':')[1])
|
| 188 |
if now_cnt == cur:
|