Solve.py

"""
Solve.py - Main file for the AlphaGeometry system

This is the main entry point that coordinates all components:
- Reads GeoGebra files
- Parses relation files
- Creates problem objects
- Runs deductive database
- Displays constructions
"""

import inspect
import os
import time
from Reading_in_Geogebra_File import parse_picture
from Read_in_Relations import parse_relations_file, create_sample_relations_file, create_sample_relations_file2
from Problem import GeometricProblem
from dd import DeductiveDatabase
from Constructions import GeometricConstructor
from ddar import DDARSystem
from verify_eqangles import verify_eqangles

#This function is a backup
def _apply_human_rabbits(problem: GeometricProblem, constructor: GeometricConstructor, rabbits_path: str, draw_marks: bool) -> None:
    """Load and apply human-provided constructions from rabbits.txt before reasoning."""
    print("\n" + "=" * 50)
    print("HUMAN RABBITS (pre-step 6):")
    print("=" * 50)

    if not os.path.exists(rabbits_path):
        print(f"human_rabbits enabled but rabbits file not found: {rabbits_path}")
        return

    with open(rabbits_path, "r") as rabbits_file:
        lines = rabbits_file.readlines()

    for idx, line in enumerate(lines, 1):
        raw = line.strip()
        if not raw or raw.startswith("#"):
            continue

        parts = raw.split()
        if len(parts) < 2:
            print(f"  [line {idx}] Skipping: need a method name and at least one point")
            continue

        method_name, *point_names = parts
        if not method_name.startswith("construct_"):
            print(f"  [line {idx}] Skipping: '{method_name}' is not a construct_ method")
            continue

        if not hasattr(constructor, method_name):
            print(f"  [line {idx}] Skipping: no such construction '{method_name}'")
            continue

        method = getattr(constructor, method_name)
        sig = inspect.signature(method)
        params = list(sig.parameters.values())[1:]  # drop self
        required_params = [
            p for p in params
            if p.default is inspect._empty and p.kind in (inspect.Parameter.POSITIONAL_ONLY, inspect.Parameter.POSITIONAL_OR_KEYWORD)
        ]
        positional_params = [
            p for p in params
            if p.kind in (inspect.Parameter.POSITIONAL_ONLY, inspect.Parameter.POSITIONAL_OR_KEYWORD)
        ]

        if len(point_names) < len(required_params):
            print(
                f"  [line {idx}] Skipping: {method_name} needs {len(required_params)} point args, got {len(point_names)}"
            )
            continue

        if len(point_names) > len(positional_params):
            print(
                f"  [line {idx}] Skipping: {method_name} accepts at most {len(positional_params)} positional args"
            )
            continue

        try:
            points = [problem.points[name] for name in point_names]
        except KeyError as e:
            print(f"  [line {idx}] Skipping: point {e} not found in problem")
            continue

        kwargs = {'name': 'M'}
        if not draw_marks:
            if "mark_points" in sig.parameters:
                kwargs["mark_points"] = False
            if "mark_point" in sig.parameters:
                kwargs["mark_point"] = False

        try:
            method(*points, **kwargs)
            print(f"  [line {idx}] Applied {method_name}({', '.join(point_names)})")
        except Exception as exc:
            print(f"  [line {idx}] {method_name} failed: {exc}")

    print("Finished human_rabbits constructions.\n")

def solve_geometric_problem(ggb_filename: str, relations_filename: str, show_construction: bool = True, use_ar: bool = True, print_reasoning: bool = False, 
                           max_iterations: int = 1000, max_ar_equations: int = None,
                           use_rabbit: bool = False, rabbit_mode: str = 'user', 
                           max_rabbit_calls: int = 1, num_random_constructions: int = 3, 
                           sanitize_on_retry: bool = False, rabbits_backup=False,
                           verify_solution: bool = False):
    """
    Main function to solve a geometric problem.
    
    Args:
        ggb_filename: Name of the .ggb file in Geogebra Files folder
        relations_filename: Name of the .txt file with relations
        show_construction: Whether to display the geometric construction
        use_ar: Whether to use integrated DDAR (DD+AR) reasoning
        max_iterations: Maximum DDAR iterations (default: 1000)
        max_ar_equations: Skip AR if more than this many equations (default: None = no limit)
        use_rabbit: Enable rabbit generation when DDAR reaches fixed point (default: False)
        rabbit_mode: 'user' (prompt), 'llm' (AI), or 'random' (random constructions) (default: 'user')
        max_rabbit_calls: Maximum number of rabbit generation calls (default: 1)
        num_random_constructions: Number of random constructions to try in 'random' mode (default: 3)
        sanitize_on_retry: Remove constructed points when retrying after failed round (default: False)
        rabbits_backup: Apply constructions from rabbits.txt before reasoning (manual backup path)
    """
    # Extract problem name from filenames for verification output
    problem_name = os.path.splitext(ggb_filename)[0]
    verification_filename = f"verification_{problem_name}.txt"
    
    start_time = time.time()
    
    print(f"🔍 SOLVING GEOMETRIC PROBLEM")
    print("="*60)
    print(f"GeoGebra file: {ggb_filename}")
    print(f"Relations file: {relations_filename}")
    print(f"Using DDAR (DD+AR): {use_ar}")
    if use_ar:
        print(f"Max iterations: {max_iterations}")
        if max_ar_equations:
            print(f"Max AR equations: {max_ar_equations}")
        if use_rabbit:
            print(f"Rabbit generation: ENABLED (mode={rabbit_mode}, max_calls={max_rabbit_calls})")
            if rabbit_mode == 'random':
                print(f"  Random constructions per attempt: {num_random_constructions}")
            if sanitize_on_retry:
                print(f"  Sanitization on retry: ENABLED")
        else:
            print(f"Rabbit generation: DISABLED")
    print("="*60)
    
    # Step 1: Parse GeoGebra file
    if ggb_filename != "":
        try:
            points_dict, lines_dict, circles_dict = parse_picture(ggb_filename)
            print(f"Loaded geometry: {len(points_dict)} points, {len(lines_dict)} lines, {len(circles_dict)} circles")
        except Exception as e:
            print(f"Error parsing GeoGebra file: {e}")
            return False
    else:
        print("No GeoGebra file provided.")
        return False
    
    # Step 2: Create problem object
    problem = GeometricProblem()
    problem.set_geometric_data(points_dict, lines_dict, circles_dict)
    
    # Step 3: Parse relations file
    try:
        assumptions, goals = parse_relations_file(relations_filename, problem.points)
        print(f"Loaded relations: {len(assumptions)} assumptions, {len(goals)} goals")
        
        for assumption in assumptions:
            problem.add_assumption(assumption)
        for goal in goals:
            problem.add_goal(goal)
            
    except Exception as e:
        print(f"Error parsing relations file: {e}")
        return False
    
    # Step 4: Display problem info
    print("\n" + "="*50)
    print("PROBLEM SETUP:")
    print("="*50)
    print(problem)
    
    print("Assumptions:")
    for i, assumption in enumerate(problem.assumptions, 1):
        print(f"  {i}. {assumption}")
    
    print("Goals to prove:")
    for i, goal in enumerate(problem.goals, 1):
        print(f"  {i}. {goal}")
    
    # Step 5: Create constructor, optionally draw, and apply backup rabbits
    constructor = GeometricConstructor(problem)
    if show_construction:
        constructor.draw_problem()

    if rabbits_backup:
        # This is a backup; in general we use "use_rabbit" parameter
        rabbits_path = os.path.join(os.path.dirname(__file__), "rabbits.txt")
        _apply_human_rabbits(problem, constructor, rabbits_path, draw_marks=show_construction)
    if show_construction:
        constructor.show_construction(f"Problem: {ggb_filename}")
    # Step 6: Run reasoning system
    print("\n" + "="*60)
    print("REASONING PROCESS:")
    print("="*60)
    
    if use_ar:
        # Use integrated DDAR system
        ddar = DDARSystem(
            max_iterations=max_iterations,
            max_ar_equations=max_ar_equations,
            use_rabbit=use_rabbit,
            rabbit_mode=rabbit_mode,
            max_rabbit_calls=max_rabbit_calls,
            num_random_constructions=num_random_constructions,
            sanitize_on_retry=sanitize_on_retry
        )
        try:
            solved, trace, all_facts = ddar.solve_problem(problem)
        except KeyboardInterrupt:
            print("\n⏹️ Interrupted by user (Ctrl+C). Running verification on current derivations...")
            if verify_solution:
                try:
                    verify_eqangles(problem, verification_filename)
                    print(f"Verification written to {verification_filename}")
                except Exception as e:
                    print(f"Eqangle verification failed: {e}")
            return False
        
        # Step 7: Final results
        print("\n" + "="*60)
        print("FINAL RESULTS:")
        print("="*60)
        
        if solved:
            print("🎉 PROBLEM SOLVED by DDAR!")
            
            # Show which goals were solved
            solved_goals = []
            for goal in problem.goals:
                if any(str(goal) == str(fact) for fact in all_facts):
                    solved_goals.append(goal)
            
            print(f"Goals proven ({len(solved_goals)}/{len(problem.goals)}):")
            for goal in solved_goals:
                print(f"  ✓ {goal}")
            
            print(f"\nReasoning used {len(trace)} steps:")
            dd_steps = sum(1 for t in trace if not t.startswith("AR:"))
            ar_steps = sum(1 for t in trace if t.startswith("AR:"))
            print(f"  DD steps: {dd_steps}")
            print(f"  AR steps: {ar_steps}")
            
            if verify_solution:
                # Verify eqangles against the diagram and write report
                try:
                    verify_eqangles(problem, verification_filename)
                    print(f"Verification written to {verification_filename}")
                except Exception as e:
                    print(f"Eqangle verification failed: {e}")
        else:
            print("❌ PROBLEM NOT SOLVED by DDAR")
            
            # Show partial progress
            if len(all_facts) > len(problem.assumptions):
                new_facts = len(all_facts) - len(problem.assumptions)
                print(f"However, {new_facts} new facts were derived during reasoning.")
                
            if verify_solution:
                # Verify eqangles against the diagram and write report
                try:
                    verify_eqangles(problem, verification_filename)
                    print(f"Verification written to {verification_filename}")
                except Exception as e:
                    print(f"Eqangle verification failed: {e}")
        if print_reasoning:
            print("\nReasoning Steps:")
            problem.pretty_print_reasoning_steps()
        return solved
    else:
        # Use DD only (legacy mode)
        dd = DeductiveDatabase()
        derived, applied_rules = dd.apply_rules(problem, use_ar=False)
        
        goals_str = set(str(g) for g in problem.goals)
        solved = any(g in [str(d) for d in derived] for g in goals_str)
        
        print("\n" + "="*60)
        print("FINAL RESULTS:")
        print("="*60)
        
        if solved:
            print("🎉 PROBLEM SOLVED by DD only!")
            solved_goals = []
            for goal in problem.goals:
                if any(str(goal) == str(d) for d in derived):
                    solved_goals.append(goal)
            
            print(f"Goals proven ({len(solved_goals)}/{len(problem.goals)}):")
            for goal in solved_goals:
                print(f"  ✓ {goal}")
            
            print(f"\nDD rules used: {len(applied_rules)}")
        else:
            print("❌ PROBLEM NOT SOLVED by DD only")
        
        end_time = time.time()
        elapsed_time = end_time - start_time
        print(f"\n  Total execution time: {elapsed_time:.4f} seconds")
        
        return solved



def create_test_problems():
    """Create sample test files for the problems from Problem 5."""
    
    # Create Geogebra Files directory if it doesn't exist
    geogebra_dir = os.path.join(os.path.dirname(__file__), "Geogebra Files")
    os.makedirs(geogebra_dir, exist_ok=True)
    
    # Create sample relations files
    create_sample_relations_file("test_files/problem5_1.txt")
    create_sample_relations_file2("test_files/problem5_2.txt")
    
    print("Sample test files created!")


if __name__ == "__main__":
    # Create test problems if needed
    create_test_problems()
    
    # Example usage
    print("AlphaGeometry System")
    print("===================")
    
    # Try to solve the first problem from Problem 5
    try:
        print("\nAttempting to solve Problem 3:")
        success3 = False #solve_geometric_problem("problem_3.ggb", "final_problems/problem_3.txt", show_construction=False, use_ar=True, print_reasoning=True, rabbit_mode='random', use_rabbit=True, max_rabbit_calls=2)
    except Exception as e:
        print(f"Error solving Problem 3: {e}")
        success3 = False 

    try:
        print("\nAttempting to solve Problem 5:")
        success5 = solve_geometric_problem("exam_problem_5.ggb", "final_problems/exam_problem_5.txt", show_construction=False, use_ar=True, print_reasoning=True, rabbits_backup = True)
    except Exception as e:
        print(f"Error solving Problem 5: {e}")
        success5 = False    

    # try:
    #     print("\nAttempting to solve Problem 7:")
    #     success7 = solve_geometric_problem("problem_7.ggb", "final_problems/problem_7.txt", show_construction=False, use_ar=True, print_reasoning=True)
    # except Exception as e:
    #     print(f"Error solving Problem 7: {e}")
    #     success7 = False  
    
    

    # try:
    #     print("\nExam Problem 2:")
    #     success12 = solve_geometric_problem(
    #         "exam-problem2.ggb", 
    #         "test_files/exam-problem2.txt", 
    #         show_construction=False,
    #         use_ar=True,
    #         max_iterations=1000,
    #         max_ar_equations=None,
    #         use_rabbit=True,  # Set to True to enable rabbit generation
    #         rabbit_mode='user',  # Options: 'user', 'random', 'llm'
    #         max_rabbit_calls=1,
    #         num_random_constructions=3,
    #         sanitize_on_retry=False,
    #         print_reasoning=True
    #     )
    # except Exception as e:
    #     print(f"Error solving Exam 2 {e}")
    #     success12 = False


    # print("\n" + "="*50)
    # print("Summary:")
    # print(f"Problem 5.1: {'SOLVED' if success1 else 'NOT SOLVED'}")
    # print(f"Problem 5.2: {'SOLVED' if success2 else 'NOT SOLVED'}")
    # print(f"Team Problem 10_10.1: {'SOLVED' if success3 else 'NOT SOLVED'}")
    # print(f"Team Problem 10_10.2: {'SOLVED' if success4 else 'NOT SOLVED'}")
    # print(f"Team Beta Problem 1: {'SOLVED' if success5 else 'NOT SOLVED'}")
    # print(f"Team Beta Problem 5: {'SOLVED' if success6 else 'NOT SOLVED'}")
    # print(f"Team LambdaGeometry Problem 3: {'SOLVED' if success7 else 'NOT SOLVED'}")
    # print(f"Team LambdaGeometry Problem 6: {'SOLVED' if success8 else 'NOT SOLVED'}")
    # print(f"Team Edward Problem 4: {'SOLVED' if success9 else 'NOT SOLVED'}")
    # print(f"Team Edward Problem 8: {'SOLVED' if success10 else 'NOT SOLVED'}")
    # print(f"IMO 2000 - Problem 1: {'SOLVED' if success11 else 'NOT SOLVED'}")
    # print(f"IMO 2007 - Problem 4: {'SOLVED' if success12 else 'NOT SOLVED'}")
    # try:
    #     print("\nAttempting to solve test rule perp_eqangle:")
    #     success = solve_geometric_problem("dummy.ggb", "test_files/test_perp_eqangle.txt", show_construction=False)
    # except Exception as e:
    #     print(f"Error solving test rule perp_eqangle: {e}")
    #     success = False
    # print(f"Perp Eqangle: {'SOLVED' if success else 'NOT SOLVED'}")