mod common;
use common::build_af;

use pickaxe_rs::prelude::*;
use std::collections::BTreeSet;

fn naive() -> NaiveEnumerationSolver {
    NaiveEnumerationSolver
}

#[cfg(feature = "sat")]
fn sat() -> SatSolver {
    SatSolver::default()
}

#[cfg(feature = "sat")]
fn scc() -> SccDecomposingSolver {
    SccDecomposingSolver {
        inner: Box::new(sat()) as Box<dyn SemanticsSolver>,
    }
}

/// All semantics that every solver supports.
const ALL_SEMANTICS: &[Semantics] = &[
    Semantics::Grounded,
    Semantics::Complete,
    Semantics::Preferred,
    Semantics::Stable,
    Semantics::Admissible,
    Semantics::SemiStable,
    Semantics::Ideal,
    Semantics::Eager,
];

/// Unique-extension semantics (must return exactly 1).
const UNIQUE_SEMANTICS: &[Semantics] = &[Semantics::Grounded, Semantics::Ideal, Semantics::Eager];

struct TestFramework {
    name: &'static str,
    af: AbstractFramework,
}

fn test_frameworks() -> Vec<TestFramework> {
    vec![
        TestFramework {
            name: "empty",
            af: build_af(0, &[]),
        },
        TestFramework {
            name: "single unattacked",
            af: build_af(1, &[]),
        },
        TestFramework {
            name: "mutual attack",
            af: build_af(2, &[(0, 1), (1, 0)]),
        },
        TestFramework {
            name: "chain A0->A1->A2",
            af: build_af(3, &[(0, 1), (1, 2)]),
        },
        TestFramework {
            name: "odd cycle (no stable)",
            af: build_af(3, &[(0, 1), (1, 2), (2, 0)]),
        },
        TestFramework {
            name: "diamond",
            af: build_af(4, &[(0, 1), (0, 2), (1, 3), (2, 3)]),
        },
        TestFramework {
            name: "self-attacking",
            af: build_af(2, &[(0, 0), (0, 1)]),
        },
    ]
}

// --- Cross-backend find_one consistency tests ---

#[test]
fn find_one_result_is_member_of_extensions_naive() {
    find_one_result_is_member_of_extensions(&naive());
}

#[test]
#[cfg(feature = "sat")]
fn find_one_result_is_member_of_extensions_sat() {
    find_one_result_is_member_of_extensions(&sat());
}

#[test]
#[cfg(feature = "sat")]
fn find_one_result_is_member_of_extensions_scc() {
    find_one_result_is_member_of_extensions(&scc());
}

fn find_one_result_is_member_of_extensions(solver: &dyn SemanticsSolver) {
    for fw in test_frameworks() {
        for &sem in ALL_SEMANTICS {
            let all_exts = solver.extensions(&fw.af, sem);
            let one = solver.find_one(&fw.af, sem);

            if all_exts.is_empty() {
                assert!(
                    one.is_none(),
                    "{} / {:?}: find_one returned Some but extensions is empty",
                    fw.name,
                    sem,
                );
            } else {
                let ext = one.unwrap_or_else(|| {
                    panic!(
                        "{} / {:?}: find_one returned None but {} extensions exist",
                        fw.name,
                        sem,
                        all_exts.len(),
                    )
                });
                assert!(
                    all_exts.contains(&ext),
                    "{} / {:?}: find_one returned {:?} which is not in extensions {:?}",
                    fw.name,
                    sem,
                    ext,
                    all_exts,
                );
            }
        }
    }
}

#[test]
fn find_one_unique_semantics_matches_extensions_naive() {
    find_one_unique_semantics_matches_extensions(&naive());
}

#[test]
#[cfg(feature = "sat")]
fn find_one_unique_semantics_matches_extensions_sat() {
    find_one_unique_semantics_matches_extensions(&sat());
}

#[test]
#[cfg(feature = "sat")]
fn find_one_unique_semantics_matches_extensions_scc() {
    find_one_unique_semantics_matches_extensions(&scc());
}

fn find_one_unique_semantics_matches_extensions(solver: &dyn SemanticsSolver) {
    for fw in test_frameworks() {
        for &sem in UNIQUE_SEMANTICS {
            let all_exts = solver.extensions(&fw.af, sem);
            assert_eq!(
                all_exts.len(),
                1,
                "{} / {:?}: expected exactly 1 extension, got {}",
                fw.name,
                sem,
                all_exts.len(),
            );
            let one = solver.find_one(&fw.af, sem).unwrap_or_else(|| {
                panic!(
                    "{} / {:?}: find_one returned None for unique semantics",
                    fw.name, sem
                )
            });
            assert_eq!(
                one, all_exts[0],
                "{} / {:?}: find_one doesn't match the unique extension",
                fw.name, sem,
            );
        }
    }
}

#[test]
#[cfg(feature = "sat")]
fn find_one_cross_backend_agreement() {
    for fw in test_frameworks() {
        for &sem in UNIQUE_SEMANTICS {
            let naive_one = naive().find_one(&fw.af, sem);
            let sat_one = sat().find_one(&fw.af, sem);
            let scc_one = scc().find_one(&fw.af, sem);
            assert_eq!(
                naive_one, sat_one,
                "{} / {:?}: naive vs SAT find_one disagree",
                fw.name, sem,
            );
            assert_eq!(
                sat_one, scc_one,
                "{} / {:?}: SAT vs SCC find_one disagree",
                fw.name, sem,
            );
        }
    }
}

// --- Cross-backend count consistency tests ---

#[test]
fn count_matches_extensions_len_naive() {
    count_matches_extensions_len(&naive());
}

#[test]
#[cfg(feature = "sat")]
fn count_matches_extensions_len_sat() {
    count_matches_extensions_len(&sat());
}

#[test]
#[cfg(feature = "sat")]
fn count_matches_extensions_len_scc() {
    count_matches_extensions_len(&scc());
}

fn count_matches_extensions_len(solver: &dyn SemanticsSolver) {
    for fw in test_frameworks() {
        for &sem in ALL_SEMANTICS {
            let all_exts = solver.extensions(&fw.af, sem);
            let cnt = solver.count(&fw.af, sem);
            assert_eq!(
                cnt,
                all_exts.len(),
                "{} / {:?}: count ({}) != extensions().len() ({})",
                fw.name,
                sem,
                cnt,
                all_exts.len(),
            );
        }
    }
}

#[test]
fn count_unique_semantics_returns_one_naive() {
    for fw in test_frameworks() {
        for &sem in UNIQUE_SEMANTICS {
            assert_eq!(
                naive().count(&fw.af, sem),
                1,
                "{} / {:?}: naive count != 1",
                fw.name,
                sem,
            );
        }
    }
}

#[test]
#[cfg(feature = "sat")]
fn count_unique_semantics_returns_one_sat_scc() {
    for fw in test_frameworks() {
        for &sem in UNIQUE_SEMANTICS {
            assert_eq!(
                sat().count(&fw.af, sem),
                1,
                "{} / {:?}: sat count != 1",
                fw.name,
                sem,
            );
            assert_eq!(
                scc().count(&fw.af, sem),
                1,
                "{} / {:?}: scc count != 1",
                fw.name,
                sem,
            );
        }
    }
}

#[test]
#[cfg(feature = "sat")]
fn count_cross_backend_agreement() {
    for fw in test_frameworks() {
        for &sem in ALL_SEMANTICS {
            let naive_cnt = naive().count(&fw.af, sem);
            let sat_cnt = sat().count(&fw.af, sem);
            let scc_cnt = scc().count(&fw.af, sem);
            assert_eq!(
                naive_cnt, sat_cnt,
                "{} / {:?}: naive count ({}) != SAT count ({})",
                fw.name, sem, naive_cnt, sat_cnt,
            );
            assert_eq!(
                sat_cnt, scc_cnt,
                "{} / {:?}: SAT count ({}) != SCC count ({})",
                fw.name, sem, sat_cnt, scc_cnt,
            );
        }
    }
}

#[test]
fn count_no_stable_on_odd_cycle_naive() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    assert_eq!(naive().count(&af, Semantics::Stable), 0);
}

#[test]
#[cfg(feature = "sat")]
fn count_no_stable_on_odd_cycle_sat_scc() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    assert_eq!(sat().count(&af, Semantics::Stable), 0);
    assert_eq!(scc().count(&af, Semantics::Stable), 0);
}

#[test]
fn find_one_no_stable_on_odd_cycle_naive() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    assert!(naive().find_one(&af, Semantics::Stable).is_none());
}

#[test]
#[cfg(feature = "sat")]
fn find_one_no_stable_on_odd_cycle_sat_scc() {
    let af = build_af(3, &[(0, 1), (1, 2), (2, 0)]);
    assert!(sat().find_one(&af, Semantics::Stable).is_none());
    assert!(scc().find_one(&af, Semantics::Stable).is_none());
}

#[test]
fn empty_framework_find_one_and_count_naive() {
    let af = build_af(0, &[]);
    for &sem in ALL_SEMANTICS {
        let naive_one = naive().find_one(&af, sem);
        assert!(
            naive_one.is_some(),
            "empty / {:?}: expected Some(empty set)",
            sem,
        );
        assert_eq!(
            naive_one.unwrap(),
            BTreeSet::new(),
            "empty / {:?}: expected empty extension",
            sem,
        );
        assert_eq!(naive().count(&af, sem), 1, "empty / {:?}: count != 1", sem);
    }
}

#[test]
#[cfg(feature = "sat")]
fn empty_framework_find_one_and_count_cross_backend() {
    let af = build_af(0, &[]);
    for &sem in ALL_SEMANTICS {
        let naive_one = naive().find_one(&af, sem);
        let sat_one = sat().find_one(&af, sem);
        assert_eq!(naive_one, sat_one, "empty / {:?}: find_one disagree", sem);
        assert_eq!(sat().count(&af, sem), 1, "empty / {:?}: count != 1", sem);
    }
}
