backend/solver.py

# solver.py
import sys
import re
import json
import os
import subprocess
from deep_convert import deep_convert
from openai import OpenAI
from dotenv import load_dotenv

def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content):
    """
    使用 sys_content + puzzle 调用模型，生成 Z3 Python 代码，
    运行并比对输出是否与 expected_solution 相同。
    """
    load_dotenv()
    client = OpenAI(
        api_key=os.getenv("GEMINI_API_KEY"),
        base_url="https://generativelanguage.googleapis.com/v1beta/openai/"
    )

    messages = [
        {"role": "user", "content": sys_content},
        {"role": "user", "content": puzzle + f'\nCategories: {str(expected_solution["header"][1:])}\n'},
    ]
    attempts = 0
    current_solution = None

    while attempts < 3:
        messages.append({"role": "user", "content": "Make sure you stick to the given categories with strictly identical names otherwise there will be a critical error."})
        attempts += 1
        response = client.chat.completions.create(
            model="gemini-2.0-flash",
            messages=messages,
            temperature=0.0,
            stream=False
        )
        content = response.choices[0].message.content
        messages.append(response.choices[0].message)

        # 提取 code
        code_blocks = re.findall(r"```(?:python)?(.*?)```", content, re.DOTALL)
        if not code_blocks:
            messages.append({"role": "user", "content": "Please write a complete Python code in your response. Try again."})
            continue

        code_to_run = code_blocks[-1].strip()
        result = subprocess.run(
            [sys.executable, "-c", code_to_run],
            stdout=subprocess.PIPE,
            stderr=subprocess.PIPE,
            text=True
        )
        output = result.stdout.strip()
        # print(output)

        if result.stderr.strip():
            messages.append({"role": "user", "content": f"Your code has errors: {result.stderr.strip()}. Please check your code and provide the complete code in the end."})
            continue

        try:
            current_solution = json.loads(output)
        except json.JSONDecodeError:
            messages.append({"role": "user", "content": "Your output is not valid JSON. Please ensure your code prints the solution as a JSON dictionary."})
            continue

        if 'rows' in current_solution.keys() and current_solution['rows'] == deep_convert(expected_solution)['rows']:
            return {
                "index": index,
                "success": True,
                "solution": current_solution,
                "attempts": attempts,
                "generatedCode": code_to_run,
                "modelResponse": content,
                "problematicConstraints": None
            }
        else:
            messages.append({"role": "user", "content": "The solution does not match the expected answer. Please check your categories and step by step reason your constraints and provide the complete code in the end."})

    if result.stderr.strip():
        return {
            "index": index,
            "success": False,
            "solution": current_solution,
            "attempts": attempts,
            "generatedCode": code_to_run,
            "modelResponse": content,
            "problematicConstraints": "Code error:\n" + result.stderr.strip()
        }

    # if 'rows' not in current_solution.keys():
    #     return {
    #         "index": index,
    #         "success": False,
    #         "solution": current_solution,
    #         "attempts": attempts,
    #         "generatedCode": code_to_run,
    #         "modelResponse": content,
    #         "problematicConstraints": str(current_solution)
    #     }

    code_by_line = code_to_run.split("\n")

    fisrt_cons_line = None
    last_cons_line = None
    for i, line in enumerate(code_by_line):
        if "s.add" in line and "pos" in line:
            if not fisrt_cons_line:
                fisrt_cons_line = i
            last_cons_line = i
    
    experiment_code_line = code_by_line[:fisrt_cons_line]
    categories = expected_solution['header']
    for i, houses in enumerate(expected_solution['rows']):
        for j in range(1, len(houses)):
            experiment_code_line.append(f"s.add(pos(\"{categories[j]}\", \"{houses[j]}\") == {i+1})")
    experiment_code_line.append("")
    experiment_code_line.append("print(s.check())")

    def satisfied(constraint):
        experiment_code_line[-2] = constraint
        experiment_code = "\n".join(experiment_code_line)
        sat_checker = experiment_code.strip()
        result = subprocess.run(
            [sys.executable, "-c", sat_checker],
            stdout=subprocess.PIPE,
            stderr=subprocess.PIPE,
            text=True
        )
        if result.stderr.strip():
            return "error: " + result.stderr.strip()
        output = result.stdout.strip()
        return output.lower()

    if "error" in current_solution.keys():
        if "Multiple" in current_solution['error']:
            problematic_constraints = "Issue: Multiple solutions\n"
        else:
            problematic_constraints = "Issue: No solution\n"
    else:
        problematic_constraints = "Issue: Wrong answer\n"

    cnt_cons = 0
    ok_satisfied = True
    problematic_constraints += "\nSatisfaction judge:\n"
    for i, line in enumerate(code_by_line):
        if "s.add" in line and "pos" in line:
            constraint = line.strip()
            cnt_cons += 1
            output = satisfied(constraint)
            if "error" in output:
                problematic_constraints += f"Error when checking {cnt_cons}-th constraint: {output}.\n"
                ok_satisfied = False
                break
            if output == "unsat":
                ok_satisfied = False
                problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
    if ok_satisfied:
        problematic_constraints += "All constraints are satisfied.\n"

    # with open("Sat_cnt.txt", "r") as f:
    #     sat_cnt = f.read()
    # Cannot directly load because the server strucutre

    cnt_cons = 0
    problematic_constraints += "\nRedundency judge:\n"
    code_by_line_experiment = code_to_run.split("\n")[:last_cons_line + 1]
    code_by_line_experiment.append("\n")
    def run_result():
        experiment_code = "\n".join(code_by_line_experiment) + sat_cnt_content
        sat_checker = experiment_code.strip()
        result = subprocess.run(
            [sys.executable, "-c", sat_checker],
            stdout=subprocess.PIPE,
            stderr=subprocess.PIPE,
            text=True
        )
        return result.stdout.strip()
    res = run_result()
    # print("\n".join(code_by_line_experiment) + sat_cnt_content)
    # print(res)
    if not res or res == "error":
        problematic_constraints += f"Unable to judge."
    else:
        cur = int(res.split(':')[1])
        problematic_constraints += f"The number of solutions: {cur}\n"
        for i, line in enumerate(code_by_line):
            if "s.add" in line and "pos" in line:
                cnt_cons += 1
                code_by_line_experiment[i] = ""
                res = run_result()
                if not res or res == "error":
                    problematic_constraints += f"Unable to judge further."
                    break
                now_cnt = int(res.split(':')[1])
                if now_cnt == cur:
                    problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {line}. A suspect redundency.\n"
                code_by_line_experiment[i] = line

    return {
        "index": index,
        "success": False,
        "solution": current_solution,
        "attempts": attempts,
        "generatedCode": code_to_run,
        "modelResponse": content,
        "problematicConstraints": problematic_constraints
    }