run_experiments_python.py

import os
import subprocess
import csv
import time
import re
import argparse
from tqdm import tqdm  # progress bar


# ============================================================
# CONFIGURATION
# ============================================================

# ASP / Clingo
ASP_PROGRAM = "political_districting.lp"
ASP_BENCHMARK_DIR = "benchmarks"
TIMEOUT_SECONDS_CLINGO = 300
PYTHON_TIMEOUT_SAFETY_MARGIN = 30

CLINGO_CONFIGS = {
    "default": [],
}

CLINGO_MODEL_COUNT = "0"
CLINGO_QUIET_OPTION = ["--quiet=1"]

# MiniZinc
MINIZINC_BIN = r"C:\Program Files\MiniZinc\minizinc.exe"
MINIZINC_MODEL = "political_districting.mzn"
MZN_BENCHMARK_DIR = "benchmarks_dzn"
MINIZINC_TIMEOUT = 300

# Results
RESULTS_FILE = "results_python.csv"


# ============================================================
# PARSING HELPERS
# ============================================================

def parse_clingo_summary(output_text, clingo_return_code, python_timed_out):
    status = "UNKNOWN"
    max_reps_val = "NA"
    num_models_val = "NA"
    raw_opt_val = "NA"

    if python_timed_out:
        status = "PYTHON_SAFETY_TIMEOUT"
    elif "INTERRUPTED" in output_text:
        status = "CLINGO_TIMEOUT_INTERRUPT"
    elif "OPTIMUM FOUND" in output_text:
        status = "OPTIMUM_FOUND"
    elif "SATISFIABLE" in output_text:
        status = "SATISFIABLE"
    elif "UNSATISFIABLE" in output_text:
        status = "UNSATISFIABLE"
    elif clingo_return_code not in [0, 10, 20, 30]:
        status = f"CLINGO_ERROR_CODE_{clingo_return_code}"
    elif clingo_return_code == 0:
        status = "UNKNOWN_EXIT_0"

    opt_match = re.search(r"Optimization\s*:\s*(-?\d+)", output_text)
    if opt_match:
        raw_opt_val = int(opt_match.group(1))
        max_reps_val = -raw_opt_val

    models_match = re.search(r"Models\s*:\s*(\S+)", output_text)
    if models_match:
        num_models_val = models_match.group(1)

    return status, max_reps_val, num_models_val, raw_opt_val


def parse_minizinc_output(output_text, exit_code, python_timed_out):
    status = "UNKNOWN"
    reps = "NA"

    if python_timed_out:
        return "PYTHON_SAFETY_TIMEOUT", reps

    if "Representatives for party" in output_text:
        status = "SATISFIABLE"

    m = re.search(r"Representatives for party\s+\d+\s*:\s*(\d+)", output_text)
    if m:
        reps = int(m.group(1))

    return status, reps


# ============================================================
# SOLVER RUNNERS
# ============================================================

def check_solver_available(name, command):
    """
    Checks whether a solver is available by trying to run '<command> --version'.
    Returns True if available, False otherwise.
    """
    try:
        process = subprocess.run(
            [command, "--version"],
            capture_output=True,
            text=True,
            timeout=5
        )
        if process.returncode == 0:
            print(f"[OK] {name} found: {command}")
            print(f"     Version: {process.stdout.strip()}")
            return True
        else:
            print(f"[WARN] {name} returned non-zero exit code when checking version.")
            print(f"       Command: {command}")
            print(f"       Output: {process.stdout.strip()}")
            return False

    except FileNotFoundError:
        print(f"[ERROR] {name} not found: {command}")
        print("        The executable does not exist or is not on PATH.")
        return False

    except Exception as e:
        print(f"[ERROR] Unexpected error while checking {name}: {e}")
        return False

def run_clingo(instance_path, party, strategy_name, strategy_options_list, dry_run=False):
    command = [
        "clingo",
        ASP_PROGRAM,
        instance_path,
        f"-c party_to_optimize={party}",
        f"--time-limit={TIMEOUT_SECONDS_CLINGO}",
    ]
    command.extend(CLINGO_QUIET_OPTION)
    command.append(CLINGO_MODEL_COUNT)
    command.extend(strategy_options_list)

    if dry_run:
        print("DRY RUN — Clingo:", " ".join(command))
        return None

    start_time = time.perf_counter()
    python_timeout = False
    output_text = ""
    exit_code = "NA"

    try:
        process = subprocess.run(
            command,
            capture_output=True,
            text=True,
            timeout=TIMEOUT_SECONDS_CLINGO + PYTHON_TIMEOUT_SAFETY_MARGIN,
            check=False
        )
        output_text = process.stdout + "\n---\n" + process.stderr
        exit_code = process.returncode

    except subprocess.TimeoutExpired:
        python_timeout = True
        output_text = "Execution timed out by Python script."
    except FileNotFoundError:
        output_text = "Clingo executable not found."
        exit_code = "FNF_ERROR"
    except Exception as e:
        output_text = f"Python error: {str(e)}"
        exit_code = "PYTHON_SUBPROC_ERROR"

    elapsed = time.perf_counter() - start_time

    status, max_reps, num_models, raw_opt = parse_clingo_summary(
        output_text, exit_code, python_timeout
    )

    return {
        "solver": "clingo",
        "strategy": strategy_name,
        "party": party,
        "max_reps": max_reps,
        "time_sec": elapsed,
        "status": status,
        "models": num_models,
        "exit_code": exit_code,
        "raw_opt": raw_opt,
    }


def run_minizinc(instance_path, party, dry_run=False):
    command = [
        MINIZINC_BIN,
        "-D", f"party_to_optimize={party}",
        MINIZINC_MODEL,
        instance_path,
        "--time-limit", str(MINIZINC_TIMEOUT * 1000),
    ]

    if dry_run:
        print("DRY RUN — MiniZinc:", " ".join(command))
        return None

    start_time = time.perf_counter()
    python_timeout = False
    output_text = ""
    exit_code = "NA"

    try:
        process = subprocess.run(
            command,
            capture_output=True,
            text=True,
            timeout=MINIZINC_TIMEOUT + PYTHON_TIMEOUT_SAFETY_MARGIN,
            check=False
        )
        output_text = process.stdout + "\n---\n" + process.stderr
        exit_code = process.returncode

    except subprocess.TimeoutExpired:
        python_timeout = True
        output_text = "Execution timed out by Python script."
    except FileNotFoundError:
        output_text = "MiniZinc executable not found."
        exit_code = "FNF_ERROR"
    except Exception as e:
        output_text = f"Python error: {str(e)}"
        exit_code = "PYTHON_SUBPROC_ERROR"

    elapsed = time.perf_counter() - start_time

    status, reps = parse_minizinc_output(output_text, exit_code, python_timeout)

    return {
        "solver": "minizinc",
        "strategy": "minizinc",
        "party": party,
        "max_reps": reps,
        "time_sec": elapsed,
        "status": status,
        "models": "NA",
        "exit_code": exit_code,
        "raw_opt": "NA",
    }


# ============================================================
# SUMMARY REPORT
# ============================================================

def print_summary(summary):
    print("\n" + "=" * 60)
    print("SUMMARY REPORT")
    print("=" * 60)

    for solver in summary:
        print(f"\nSolver: {solver}")
        print(f"  Runs: {summary[solver]['count']}")
        print(f"  SAT: {summary[solver]['sat']}")
        print(f"  UNSAT: {summary[solver]['unsat']}")
        print(f"  TIMEOUTS: {summary[solver]['timeout']}")
        if summary[solver]['count'] > 0:
            avg = summary[solver]['total_time'] / summary[solver]['count']
        else:
            avg = 0
        print(f"  Avg Time: {avg:.3f}s")

    print("\n" + "=" * 60 + "\n")


# ============================================================
# MAIN LOOP
# ============================================================

def main():
    parser = argparse.ArgumentParser(
        description="Run ASP and MiniZinc experiments with progress bar and summary report.",
        formatter_class=argparse.RawTextHelpFormatter
    )

    parser.add_argument(
        "--solver",
        choices=["asp", "minizinc", "both"],
        default="both",
        help="Choose which solver(s) to run."
    )

    parser.add_argument(
        "--dry-run",
        action="store_true",
        help="Print commands without executing them."
    )

    args = parser.parse_args()

    print("Checking solver availability...\n")

    clingo_ok = check_solver_available("Clingo", "clingo")
    minizinc_ok = check_solver_available("MiniZinc", MINIZINC_BIN)

    print()  # blank line

    if run_asp and not clingo_ok:
        print("Clingo is required but not available. Aborting.")
        return

    if run_mzn and not minizinc_ok:
        print("MiniZinc is required but not available. Aborting.")
        return


    run_asp = args.solver in ("asp", "both")
    run_mzn = args.solver in ("minizinc", "both")

    write_header = not os.path.isfile(RESULTS_FILE)

    summary = {
        "clingo": {"count": 0, "sat": 0, "unsat": 0, "timeout": 0, "total_time": 0},
        "minizinc": {"count": 0, "sat": 0, "unsat": 0, "timeout": 0, "total_time": 0},
    }

    asp_instances = sorted(
        f for f in os.listdir(ASP_BENCHMARK_DIR)
        if f.endswith(".lp")
    )

    mzn_instances = sorted(
        f for f in os.listdir(MZN_BENCHMARK_DIR)
        if f.endswith(".dzn")
    )

    total_runs = (
        len(asp_instances) * 2 * (1 if run_asp else 0) +
        len(mzn_instances) * 2 * (1 if run_mzn else 0)
    )

    with open(RESULTS_FILE, 'a', newline='') as csvfile:
        csv_writer = csv.writer(csvfile)
        if write_header:
            csv_writer.writerow([
                "Instance", "PartyOptimized", "Strategy",
                "MaxReps", "TimeSec", "Status",
                "Models", "SolverReturnCode", "RawOptValue"
            ])

        with tqdm(total=total_runs, desc="Running experiments") as pbar:

            # ---------------- ASP LOOP ----------------
            if run_asp:
                for instance_filename in asp_instances:
                    instance_path = os.path.join(ASP_BENCHMARK_DIR, instance_filename)

                    for party in [0, 1]:
                        for strategy_name, strategy_opts in CLINGO_CONFIGS.items():
                            res = run_clingo(instance_path, party, strategy_name, strategy_opts, args.dry_run)
                            if res:
                                csv_writer.writerow([
                                    instance_filename, party, res["strategy"],
                                    res["max_reps"], f"{res['time_sec']:.3f}",
                                    res["status"], res["models"],
                                    res["exit_code"], res["raw_opt"]
                                ])
                                summary["clingo"]["count"] += 1
                                summary["clingo"]["total_time"] += res["time_sec"]
                                if res["status"] in ("SATISFIABLE", "OPTIMUM_FOUND"):
                                    summary["clingo"]["sat"] += 1
                                elif res["status"] == "UNSATISFIABLE":
                                    summary["clingo"]["unsat"] += 1
                                elif "TIMEOUT" in res["status"]:
                                    summary["clingo"]["timeout"] += 1
                            pbar.update(1)

            # ---------------- MINIZINC LOOP ----------------
            if run_mzn:
                for instance_filename in mzn_instances:
                    instance_path = os.path.join(MZN_BENCHMARK_DIR, instance_filename)

                    for party in [0, 1]:
                        res = run_minizinc(instance_path, party, args.dry_run)
                        if res:
                            csv_writer.writerow([
                                instance_filename, party, res["strategy"],
                                res["max_reps"], f"{res['time_sec']:.3f}",
                                res["status"], res["models"],
                                res["exit_code"], res["raw_opt"]
                            ])
                            summary["minizinc"]["count"] += 1
                            summary["minizinc"]["total_time"] += res["time_sec"]
                            if res["status"] == "SATISFIABLE":
                                summary["minizinc"]["sat"] += 1
                            elif res["status"] == "UNSATISFIABLE":
                                summary["minizinc"]["unsat"] += 1
                            elif "TIMEOUT" in res["status"]:
                                summary["minizinc"]["timeout"] += 1
                        pbar.update(1)

    print_summary(summary)
    print(f"Results saved to {RESULTS_FILE}")


if __name__ == "__main__":
    main()