//! The classic "Tweety Triangle" — a standard benchmark for structured
//! argumentation systems.
//!
//! Tweety is a bird and a penguin. Birds defeasibly fly, but penguins
//! strictly don't fly. With last-link elitist ordering and the strict rule
//! ranked above the defeasible rule, the grounded extension should contain
//! the argument for ¬flies(tweety) but not flies(tweety).
//!
//! Run with: `cargo run --example tweety`

use pickaxe_rs::prelude::*;

fn main() {
    // ── 1. Build the ASPIC+ system ──────────────────────────────────────

    let (system, warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(penguin(tweety)))
        .defeasible_rule("d1", vec![formula!(bird(tweety))], formula!(flies(tweety)))
        .strict_rule(
            "s1",
            vec![formula!(penguin(tweety))],
            formula!(bird(tweety)),
        )
        .strict_rule(
            "s2",
            vec![formula!(penguin(tweety))],
            formula!(!flies(tweety)),
        )
        .with_classical_negation()
        .build();

    println!("System built with {} warning(s).", warnings.len());
    for w in &warnings {
        println!("  warning: {w:?}");
    }

    // ── 2. Configure preferences ────────────────────────────────────────

    // Rank the strict rule's identifier above the defeasible rule.
    let rule_ord = TieredOrdering::new(vec![vec![RuleId("s2".into())], vec![RuleId("d1".into())]]);

    let ordering: Box<dyn ArgumentOrdering> = Box::new(LastLinkOrdering {
        rule_ordering: Box::new(rule_ord),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    });

    // ── 3. Run the pipeline ─────────────────────────────────────────────

    let pipeline = AspicPipeline::classical(system, ordering);
    let result = pipeline
        .evaluate(Semantics::Grounded)
        .expect("pipeline evaluation failed");

    // ── 4. Inspect results ──────────────────────────────────────────────

    println!(
        "\nGrounded extension has {} argument(s):",
        result.extensions[0].len()
    );

    for &arg_id in &result.extensions[0] {
        let arg = result.store.get(arg_id).unwrap();
        let kind = if arg.is_strict(&result.store) {
            "strict"
        } else {
            "defeasible"
        };
        println!("  A{}: {} ({})", arg_id.0, arg.conclusion(), kind);
    }

    // ── 5. Export the abstract framework ────────────────────────────────

    let af = AbstractFramework::from_defeats(&result.store, &[]);
    println!("\nAbstract framework (TGF):\n{}", af.to_tgf());
}
