//! # pickaxe-rs
//!
//! A Rust library implementing the
//! [ASPIC+](https://doi.org/10.1016/j.artint.2012.10.008) framework for
//! structured argumentation (Modgil & Prakken, 2014), with the Prakken (2019)
//! accrual extension.
//!
//! ASPIC+ is a formal framework for constructing arguments from a knowledge
//! base of premises and inference rules, identifying attacks between those
//! arguments, and evaluating which arguments are ultimately acceptable under
//! Dung-style semantics. This crate provides a faithful, modular
//! implementation of the full ASPIC+ lifecycle: grounding, argument
//! construction, attack identification, defeat computation (with configurable
//! preference orderings), and semantics evaluation.
//!
//! The language is restricted to the **Bernays-Schoenfinkel fragment** of
//! first-order logic (function-free terms, universally quantified variables
//! over a finite Herbrand universe). This keeps grounding decidable and
//! guarantees termination. After grounding, the system is effectively
//! propositional.
//!
//! # Quick start
//!
//! ```
//! use pickaxe_rs::prelude::*;
//!
//! // Build a system: Tweety is a bird and a penguin.
//! // Birds defeasibly fly, but penguins strictly don't.
//! 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();
//!
//! // Define a preference: s2 (strict) is more preferred than d1 (defeasible).
//! 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,
//! });
//!
//! // Run the pipeline under grounded semantics.
//! let pipeline = AspicPipeline::classical(system, ordering);
//! let result = pipeline.evaluate(Semantics::Grounded).unwrap();
//!
//! assert_eq!(result.extensions.len(), 1);
//! ```
//!
//! # Pipeline architecture
//!
//! The evaluation pipeline has four stages, each defined by a swappable trait:
//!
//! 1. **[`Grounder`](pipeline::traits::Grounder)** — eliminates first-order
//!    variables via Herbrand substitution, producing a
//!    [`GroundedSystem`](language::grounding::GroundedSystem).
//! 2. **[`ArgumentConstructor`](pipeline::traits::ArgumentConstructor)** —
//!    builds the set of all derivable ASPIC+ arguments in an
//!    [`ArgumentStore`](framework::argument_store::ArgumentStore).
//! 3. **[`AttackComputer`](pipeline::traits::AttackComputer)** — identifies
//!    rebut, undermine, and undercut
//!    [`Attack`](framework::attack::Attack)s between arguments.
//! 4. **[`Evaluator`](pipeline::traits::Evaluator)** — computes defeats
//!    (applying preference orderings), builds an
//!    [`AbstractFramework`](framework::abstract_af::AbstractFramework), and
//!    solves for extensions under a chosen
//!    [`Semantics`](framework::semantics::Semantics).
//!
//! The pipeline is orchestrated by [`AspicPipeline`](pipeline::AspicPipeline).
//! Three convenience constructors wire up common configurations:
//!
//! - [`AspicPipeline::classical`](pipeline::AspicPipeline::classical) — naive
//!   implementations at every stage.
//! - [`AspicPipeline::optimised`](pipeline::AspicPipeline::optimised) — indexed
//!   attack computation and SCC-decomposing SAT solver (requires `sat` feature).
//! - [`AspicPipeline::accrual`](pipeline::AspicPipeline::accrual) — accrual
//!   evaluation with set-level preferences (Prakken, 2019).
//!
//! # Modules
//!
//! - [`language`] — formula representation, the [`formula!`] macro, and
//!   grounding infrastructure.
//! - [`system`] — the [`AspicSystem`](system::AspicSystem) definition:
//!   knowledge base, rules, contrariness, and preference orderings. Start
//!   here with [`AspicSystemBuilder`](system::builder::AspicSystemBuilder).
//! - [`framework`] — the argumentation framework layer: arguments, attacks,
//!   the abstract framework, and semantics (extensions and labellings).
//! - [`pipeline`] — the four-stage evaluation pipeline, its trait
//!   abstractions, concrete implementations, and configuration.
//! - [`io`] — serialisation formats: simple JSON, native structured format,
//!   and AF export (TGF, ASPARTIX, DOT, ICCMA).
//! - [`algorithms`] — generic graph algorithms (Tarjan's SCC, Kahn's
//!   topological sort, maximal-set computation) used internally.
//! - [`error`] — the [`AspicError`](error::AspicError) hierarchy.
//!
//! # Feature flags
//!
//! - **`sat`** *(default)* — enables [`SatSolver`](pipeline::evaluation::sat_solver::SatSolver),
//!   [`SccDecomposingSolver`](pipeline::evaluation::scc_solver::SccDecomposingSolver),
//!   [`IndexedAttackComputer`](pipeline::attack::IndexedAttackComputer), and
//!   the [`optimised`](pipeline::AspicPipeline::optimised) preset. Default
//!   SAT backend is BatSat.
//! - **`cadical`** — adds CaDiCaL as an alternative SAT backend (implies `sat`).
//! - **`json`** *(default)* — JSON serialisation via `serde_json`.
//! - **`toml-ser`** *(default)* — TOML serialisation via `toml`.
//! - **`aspartix`** — enables
//!   [`AspartixSolver`](pipeline::evaluation::aspartix_solver::AspartixSolver),
//!   which shells out to [clingo](https://potassco.org/clingo/).
//! - **`iccma`** — enables
//!   [`IccmaSolver`](pipeline::evaluation::iccma_solver::IccmaSolver) for
//!   ICCMA-compatible external solvers.
//! - **`cli`** — builds the `pickaxe` command-line binary (implies `json`, package name `pickaxe-rs`).

#![cfg_attr(docsrs, feature(doc_cfg))]
// Pedantic clippy policy: domain-specific names (attacker/attacked) trigger
// similar_names; module_name_repetitions is standard Rust API style;
// must_use on every pure accessor is too noisy for a research library;
// implicit_hasher penalises concrete HashMap/HashSet params in internal APIs;
// match_same_arms and wildcard_enum are fine for exhaustive enum matches;
// trivially_copy_pass_by_ref on &bool/&u8 is not worth the churn.
#![allow(
    clippy::similar_names,
    clippy::module_name_repetitions,
    clippy::must_use_candidate,
    clippy::return_self_not_must_use,
    clippy::implicit_hasher,
    clippy::trivially_copy_pass_by_ref,
    clippy::match_same_arms,
    clippy::wildcard_enum_match_arm,
    clippy::needless_pass_by_value,
    clippy::unused_self,
    clippy::too_many_lines
)]

#[macro_use]
pub mod language;
pub mod algorithms;
pub mod error;
pub mod framework;
pub mod io;
pub mod pipeline;
pub mod system;

/// Convenience re-exports for the most commonly used types and traits.
///
/// A `use pickaxe_rs::prelude::*;` pulls in everything needed for typical
/// system construction, pipeline evaluation, and result inspection.
///
/// ## Feature-gated symbols
///
/// The following symbols are only available when the corresponding Cargo
/// feature is enabled:
///
/// | Feature      | Symbols                                      |
/// |--------------|----------------------------------------------|
/// | `sat`        | `SatSolver`, `SccDecomposingSolver`           |
/// | `aspartix`   | `AspartixSolver`                             |
/// | `iccma`      | `IccmaSolver`                                |
///
/// The [`SolverConfig`](crate::pipeline::config::SolverConfig) enum also gains additional variants under `sat`,
/// `cadical`, `aspartix`, and `iccma` features.
pub mod prelude {
    // ── Core: Language ──────────────────────────────────────────────────
    pub use crate::formula;
    pub use crate::language::formula::{Atom, Formula, Literal, Term};
    pub use crate::language::grounding::GroundedSystem;
    pub use crate::pipeline::grounding::{NaiveGrounder, SemiNaiveGrounder};

    // ── Core: System ────────────────────────────────────────────────────
    pub use crate::system::builder::AspicSystemBuilder;
    pub use crate::system::consistency::{
        check_contraposition_closure, is_directly_consistent, is_indirectly_consistent,
        strict_closure,
    };
    pub use crate::system::contrariness::{ContrarinessFunction, ContrarinessRelation};
    pub use crate::system::knowledge::{KnowledgeBase, Premise, PremiseKind};
    pub use crate::system::postulates::{
        check_direct_consistency, check_indirect_consistency, check_strict_closure,
        check_sub_argument_closure,
    };
    pub use crate::system::rules::{DefeasibleRule, Rule, RuleId, StrictRule};
    pub use crate::system::warning::Warning;
    pub use crate::system::AspicSystem;

    // ── Core: Arguments ─────────────────────────────────────────────────
    pub use crate::framework::argument::{Argument, ArgumentId};
    pub use crate::framework::argument_store::ArgumentStore;
    pub use crate::pipeline::construction::ForwardChainingConstructor;

    // ── Core: Attacks & Defeat ──────────────────────────────────────────
    pub use crate::framework::attack::{compute_defeats, Attack, AttackKind, Defeat};
    pub use crate::pipeline::attack::{IndexedAttackComputer, PairwiseAttackComputer};

    // ── Core: Orderings & Preference ────────────────────────────────────
    pub use crate::system::ordering::{
        lifted_strict, ArgumentOrdering, FlatOrdering, LastLinkOrdering, LiftedSetPreference,
        LiftingStrategy, NoPreference, Preference, PremiseOrdering, RuleOrdering, SetPreference,
        TieredOrdering, WeakestLinkOrdering,
    };

    // ── Core: Abstract Framework ────────────────────────────────────────
    pub use crate::framework::abstract_af::AbstractFramework;

    // ── Core: Semantics ─────────────────────────────────────────────────
    pub use crate::framework::semantics::{Extension, Label, Labelling, Semantics};

    // ── Core: Pipeline ──────────────────────────────────────────────────
    pub use crate::pipeline::config::{
        build_ordering, build_tiered_rule_ordering, ArgConstructorConfig, AttackComputerConfig,
        EvaluatorConfig, GrounderConfig, PipelineConfig, PreferenceMode, SolverConfig,
    };
    pub use crate::pipeline::evaluation::accrual::AccrualEvaluator;
    pub use crate::pipeline::evaluation::classical::ClassicalEvaluator;
    pub use crate::pipeline::evaluation::naive_solver::NaiveEnumerationSolver;
    pub use crate::pipeline::traits::{
        ArgumentConstructor, AttackComputer, EvaluationResult, Evaluator, Grounder,
        PreferenceConfig, SemanticsSolver,
    };
    pub use crate::pipeline::{AspicPipeline, PipelineResult};

    // ── Feature-gated: Solvers ──────────────────────────────────────────
    #[cfg(feature = "aspartix")]
    pub use crate::pipeline::evaluation::aspartix_solver::AspartixSolver;
    #[cfg(feature = "iccma")]
    pub use crate::pipeline::evaluation::iccma_solver::IccmaSolver;
    #[cfg(feature = "sat")]
    pub use crate::pipeline::evaluation::sat_solver::SatSolver;
    #[cfg(feature = "sat")]
    pub use crate::pipeline::evaluation::scc_solver::SccDecomposingSolver;

    // ── I/O ─────────────────────────────────────────────────────────────
    pub use crate::io::native::{NativeTheory, SerializableSystem};
    pub use crate::io::output::{ExtensionOutput, PipelineOutput, Timings, TimingsOutput};
    pub use crate::io::simple::{parse_formula, RulePreference, SimpleTheory};

    // ── Error ───────────────────────────────────────────────────────────
    pub use crate::error::{AspicError, PipelineStage, SerialError, SolverError};
}
