use std::collections::{BTreeSet, HashMap};

mod common;
use common::*;

use pickaxe_rs::formula;
#[cfg(any(feature = "json", feature = "toml-ser"))]
use pickaxe_rs::language::formula::{Atom, Literal};
use pickaxe_rs::prelude::*;
#[cfg(any(feature = "json", feature = "toml-ser"))]
use proptest::prelude::*;

// ---
// Serialization
// ---
mod serialization {
    use super::*;

    #[test]
    fn serializable_system_captures_all_fields() {
        let system = running_example();
        let ser = SerializableSystem::from_system(&system);

        assert_eq!(ser.premises.len(), 4, "4 premises: p, s, u, x");
        assert_eq!(ser.strict_rules.len(), 2, "2 strict rules: s1, s2");
        assert_eq!(ser.defeasible_rules.len(), 6, "6 defeasible rules: d1–d6");
        assert!(ser.classical_negation, "classical negation enabled");

        // Classical negation pairs are generated on-the-fly, not stored in
        // entries. The `classical_negation` flag handles reconstruction.

        let kinds: BTreeSet<&str> = ser.premises.iter().map(|p| p.kind.as_str()).collect();
        assert!(kinds.contains("axiom"), "has axiom premise");
        assert!(kinds.contains("ordinary"), "has ordinary premise");

        for dr in &ser.defeasible_rules {
            assert!(
                dr.name.is_some(),
                "all defeasible rules have names in this example"
            );
        }
    }

    #[cfg(feature = "json")]
    #[test]
    fn json_round_trip_grounded() {
        let system = running_example();
        let ser = SerializableSystem::from_system(&system);
        let json = ser.to_json().expect("JSON serialization");
        let deser = SerializableSystem::from_json(&json).expect("JSON deserialization");
        let restored = deser.to_system().unwrap();

        let orig_result = AspicPipeline::classical(system, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        let rest_result = AspicPipeline::classical(restored, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        assert_eq!(orig_result.extensions.len(), rest_result.extensions.len());
        let orig_conc = conclusions_in(&orig_result.extensions[0], &orig_result.store);
        let rest_conc = conclusions_in(&rest_result.extensions[0], &rest_result.store);
        assert_eq!(
            orig_conc, rest_conc,
            "grounded extensions must match after JSON round-trip"
        );
    }

    #[cfg(feature = "toml-ser")]
    #[test]
    fn toml_round_trip_grounded() {
        let system = running_example();
        let ser = SerializableSystem::from_system(&system);
        let toml_str = ser.to_toml().expect("TOML serialization");
        let deser = SerializableSystem::from_toml(&toml_str).expect("TOML deserialization");
        let restored = deser.to_system().unwrap();

        let orig_result = AspicPipeline::classical(system, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        let rest_result = AspicPipeline::classical(restored, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let orig_conc = conclusions_in(&orig_result.extensions[0], &orig_result.store);
        let rest_conc = conclusions_in(&rest_result.extensions[0], &rest_result.store);
        assert_eq!(
            orig_conc, rest_conc,
            "grounded extensions must match after TOML round-trip"
        );
    }

    #[cfg(feature = "json")]
    #[test]
    fn round_trip_with_nontrivial_ordering() {
        let system = running_example();
        let ser = SerializableSystem::from_system(&system);
        let json = ser.to_json().unwrap();
        let restored = SerializableSystem::from_json(&json)
            .unwrap()
            .to_system()
            .unwrap();

        // d5 > d2: d5 in tier 1 (most preferred), d2 in tier 2
        // D4 (via d5) defeats B2 (via d2), so ¬t justified, d1 survives → q, r
        let ordering_orig = last_link(
            vec![vec![RuleId("d5".into())], vec![RuleId("d2".into())]],
            vec![],
        );
        let ordering_rest = last_link(
            vec![vec![RuleId("d5".into())], vec![RuleId("d2".into())]],
            vec![],
        );

        let orig_result = AspicPipeline::classical(system, Box::new(ordering_orig))
            .evaluate(Semantics::Grounded)
            .unwrap();
        let rest_result = AspicPipeline::classical(restored, Box::new(ordering_rest))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let orig_conc = conclusions_in(&orig_result.extensions[0], &orig_result.store);
        let rest_conc = conclusions_in(&rest_result.extensions[0], &rest_result.store);
        assert_eq!(orig_conc, rest_conc);
        assert!(
            orig_conc.contains(&formula!(r)),
            "r should be in grounded extension with d5 > d2"
        );
    }

    #[cfg(feature = "json")]
    #[test]
    fn contradictory_pair_deduplication() {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .named_defeasible_rule("d1", formula!(d1), vec![], formula!(!a))
            .build();

        let ser = SerializableSystem::from_system(&system);
        let json = ser.to_json().unwrap();

        let contradictory_count = ser
            .contrariness
            .iter()
            .filter(|e| e.relation == "contradictory")
            .count();

        let pair_formulas: BTreeSet<BTreeSet<&Formula>> = ser
            .contrariness
            .iter()
            .filter(|e| e.relation == "contradictory")
            .map(|e| {
                let mut s = BTreeSet::new();
                s.insert(&e.target);
                s.insert(&e.attacker);
                s
            })
            .collect();

        assert_eq!(
            contradictory_count,
            pair_formulas.len(),
            "each contradictory pair appears exactly once"
        );

        let restored = SerializableSystem::from_json(&json)
            .unwrap()
            .to_system()
            .unwrap();
        let orig_result = AspicPipeline::classical(system, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        let rest_result = AspicPipeline::classical(restored, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let orig_conc = conclusions_in(&orig_result.extensions[0], &orig_result.store);
        let rest_conc = conclusions_in(&rest_result.extensions[0], &rest_result.store);
        assert_eq!(orig_conc, rest_conc);
    }

    #[cfg(feature = "json")]
    #[test]
    fn classical_negation_flag_preserved() {
        let (with_cn, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .build();
        let ser_cn = SerializableSystem::from_system(&with_cn);
        assert!(ser_cn.classical_negation);

        let json_cn = ser_cn.to_json().unwrap();
        let deser_cn = SerializableSystem::from_json(&json_cn).unwrap();
        assert!(deser_cn.classical_negation);

        let (without_cn, _) = AspicSystemBuilder::new()
            .ordinary_premise(formula!(a))
            .build();
        let ser_no = SerializableSystem::from_system(&without_cn);
        assert!(!ser_no.classical_negation);

        let json_no = ser_no.to_json().unwrap();
        let deser_no = SerializableSystem::from_json(&json_no).unwrap();
        assert!(!deser_no.classical_negation);
    }

    #[cfg(all(feature = "json", feature = "toml-ser"))]
    #[test]
    fn empty_system_round_trip() {
        let (system, _) = AspicSystemBuilder::new().build();
        let ser = SerializableSystem::from_system(&system);

        let json = ser.to_json().unwrap();
        let from_json = SerializableSystem::from_json(&json)
            .unwrap()
            .to_system()
            .unwrap();
        let json_result = AspicPipeline::classical(from_json, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        assert!(
            json_result.extensions[0].is_empty(),
            "empty system produces empty grounded extension (JSON)"
        );

        let toml_str = ser.to_toml().unwrap();
        let from_toml = SerializableSystem::from_toml(&toml_str)
            .unwrap()
            .to_system()
            .unwrap();
        let toml_result = AspicPipeline::classical(from_toml, Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();
        assert!(
            toml_result.extensions[0].is_empty(),
            "empty system produces empty grounded extension (TOML)"
        );
    }

    #[cfg(feature = "json")]
    #[test]
    fn round_trip_preferred_and_stable() {
        let system = running_example();
        let ser = SerializableSystem::from_system(&system);
        let json = ser.to_json().unwrap();
        let restored = SerializableSystem::from_json(&json)
            .unwrap()
            .to_system()
            .unwrap();

        // Preferred
        let orig_pref = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering))
            .evaluate(Semantics::Preferred)
            .unwrap();
        let rest_pref = AspicPipeline::classical(restored.clone(), Box::new(EqualOrdering))
            .evaluate(Semantics::Preferred)
            .unwrap();

        assert_eq!(orig_pref.extensions.len(), rest_pref.extensions.len());
        let mut orig_concs: Vec<BTreeSet<Formula>> = orig_pref
            .extensions
            .iter()
            .map(|e| conclusions_in(e, &orig_pref.store))
            .collect();
        let mut rest_concs: Vec<BTreeSet<Formula>> = rest_pref
            .extensions
            .iter()
            .map(|e| conclusions_in(e, &rest_pref.store))
            .collect();
        orig_concs.sort();
        rest_concs.sort();
        assert_eq!(orig_concs, rest_concs, "preferred extensions match");

        // Stable
        let orig_stab = AspicPipeline::classical(system, Box::new(EqualOrdering))
            .evaluate(Semantics::Stable)
            .unwrap();
        let rest_stab = AspicPipeline::classical(restored, Box::new(EqualOrdering))
            .evaluate(Semantics::Stable)
            .unwrap();

        assert_eq!(orig_stab.extensions.len(), rest_stab.extensions.len());
    }
}

// ---
// Pipeline orchestration
// ---
mod pipeline {
    use super::*;

    #[test]
    fn pipeline_result_fields_populated() {
        let result = AspicPipeline::classical(running_example(), Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        assert!(
            !result.grounded_system.knowledge_base.premises.is_empty(),
            "grounded_system has premises"
        );
        assert!(!result.store.is_empty(), "store is non-empty");
        assert!(!result.attacks.is_empty(), "attacks is non-empty");
        assert_eq!(
            result.labellings.len(),
            result.extensions.len(),
            "labellings.len() == extensions.len()"
        );
    }

    #[test]
    fn classical_pipeline_scenario_a() {
        // d5 > d2: D4 (via d5) defeats B2 (via d2), so t is not justified,
        // d1 survives, giving q, then r via s1
        let ordering = last_link(
            vec![vec![RuleId("d5".into())], vec![RuleId("d2".into())]],
            vec![],
        );
        let result = AspicPipeline::classical(running_example(), Box::new(ordering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let conc = conclusions_in(&result.extensions[0], &result.store);
        assert!(
            conc.contains(&formula!(r)),
            "r should be in grounded extension"
        );
    }

    #[test]
    fn classical_pipeline_equal_ordering() {
        let result = AspicPipeline::classical(running_example(), Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let conc = conclusions_in(&result.extensions[0], &result.store);
        assert!(
            conc.contains(&formula!(p)),
            "axiom p should be in grounded extension"
        );
        // With EqualOrdering, E (via s2: v→¬s) undermines B1 (ordinary premise s),
        // which defeats B2 (s⇒t) and B3 (t⇒¬d1), so d1 survives and r is justified.
        assert!(
            conc.contains(&formula!(r)),
            "r should be in grounded extension with equal ordering"
        );
    }

    #[cfg(feature = "sat")]
    #[test]
    fn optimised_matches_classical() {
        let classical_result = AspicPipeline::classical(running_example(), Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let optimised_result = AspicPipeline::optimised(running_example(), Box::new(EqualOrdering))
            .evaluate(Semantics::Grounded)
            .unwrap();

        let classical_conc =
            conclusions_in(&classical_result.extensions[0], &classical_result.store);
        let optimised_conc =
            conclusions_in(&optimised_result.extensions[0], &optimised_result.store);
        assert_eq!(
            classical_conc, optimised_conc,
            "optimised and classical pipelines produce same grounded extension"
        );
    }

    #[test]
    fn trait_substitutability() {
        struct EmptyGrounder;
        impl Grounder for EmptyGrounder {
            fn ground(&self, system: &AspicSystem) -> Result<GroundedSystem, AspicError> {
                Ok(GroundedSystem {
                    knowledge_base: KnowledgeBase { premises: vec![] },
                    strict_rules: vec![],
                    defeasible_rules: vec![],
                    contrariness: system.contrariness.clone(),
                })
            }
        }

        let mut pipeline = AspicPipeline::classical(running_example(), Box::new(EqualOrdering));
        pipeline.grounder = Box::new(EmptyGrounder);

        let result = pipeline.evaluate(Semantics::Grounded).unwrap();
        assert!(
            result.extensions[0].is_empty(),
            "empty grounder produces empty extension"
        );
    }

    #[test]
    fn trait_objects_are_send_sync() {
        fn assert_send_sync<T: Send + Sync>() {}

        assert_send_sync::<Box<dyn Grounder>>();
        assert_send_sync::<Box<dyn ArgumentConstructor>>();
        assert_send_sync::<Box<dyn AttackComputer>>();
        assert_send_sync::<Box<dyn Evaluator>>();
    }

    #[test]
    fn pipeline_multiple_semantics() {
        // Use NoPreference ordering (all incomparable) to get multiple preferred extensions
        let preferred_result = AspicPipeline::classical(
            running_example(),
            Box::new(LastLinkOrdering {
                rule_ordering: Box::new(NoPreference),
                premise_ordering: Box::new(NoPreference),
                lifting: LiftingStrategy::Elitist,
            }),
        )
        .evaluate(Semantics::Preferred)
        .unwrap();

        assert!(
            preferred_result.extensions.len() >= 2,
            "preferred should have multiple extensions with NoPreference"
        );
        assert_eq!(
            preferred_result.labellings.len(),
            preferred_result.extensions.len()
        );

        let stable_result = AspicPipeline::classical(
            running_example(),
            Box::new(LastLinkOrdering {
                rule_ordering: Box::new(NoPreference),
                premise_ordering: Box::new(NoPreference),
                lifting: LiftingStrategy::Elitist,
            }),
        )
        .evaluate(Semantics::Stable)
        .unwrap();

        assert!(
            !stable_result.extensions.is_empty(),
            "stable has extensions"
        );
        assert_eq!(
            stable_result.labellings.len(),
            stable_result.extensions.len()
        );
    }
}

// ---
// Export formats
// ---
mod export {
    use super::*;

    fn small_af() -> (AbstractFramework, ArgumentStore) {
        let (system, _) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .ordinary_premise(formula!(b))
            .named_defeasible_rule("d1", formula!(d1), vec![formula!(a)], formula!(!b))
            .build();

        let pipeline = AspicPipeline::classical(system, Box::new(EqualOrdering));
        let result = pipeline.evaluate(Semantics::Grounded).unwrap();

        let defeats = compute_defeats(&result.attacks, &result.store, &EqualOrdering);
        let af = AbstractFramework::from_defeats(&result.store, &defeats);
        (af, result.store)
    }

    #[test]
    fn tgf_format_conformance() {
        let (af, _store) = small_af();

        let tgf = af.to_tgf();
        let lines: Vec<&str> = tgf.lines().collect();

        let sep_pos = lines
            .iter()
            .position(|l| *l == "#")
            .expect("TGF must have # separator");
        assert!(sep_pos > 0, "arguments listed before #");

        for line in &lines[..sep_pos] {
            line.parse::<usize>()
                .expect("argument ID should be numeric");
        }

        for line in &lines[sep_pos + 1..] {
            let parts: Vec<&str> = line.split_whitespace().collect();
            assert_eq!(parts.len(), 2, "defeat line has two IDs");
        }
    }

    #[test]
    fn aspartix_format_conformance() {
        let (af, _store) = small_af();
        let apx = af.to_aspartix();

        let mut arg_count = 0;
        let mut att_count = 0;
        for line in apx.lines() {
            assert!(line.ends_with('.'), "ASPARTIX line must end with '.'");
            if line.starts_with("arg(") {
                arg_count += 1;
            } else if line.starts_with("att(") {
                att_count += 1;
            }
        }

        assert_eq!(arg_count, af.arguments.len());
        assert_eq!(att_count, af.defeats.len());
    }

    #[test]
    fn dot_format_conformance() {
        let (af, store) = small_af();
        let dot = af.to_dot(&store);

        assert!(
            dot.starts_with("digraph AF {"),
            "DOT must start with digraph"
        );
        assert!(dot.contains("node [shape=box]"), "DOT must set node shape");
        assert!(dot.contains("->"), "DOT must have edges");
        assert!(dot.trim_end().ends_with('}'), "DOT must end with '}}' ");

        for arg_id in &af.arguments {
            assert!(
                dot.contains(&format!("a{} [label=", arg_id.0)),
                "each argument must have a node declaration"
            );
        }
    }

    #[test]
    fn iccma_format_conformance() {
        let (af, _store) = small_af();
        let iccma = af.to_iccma();
        let lines: Vec<&str> = iccma.lines().collect();

        let header = lines[0];
        assert!(header.starts_with("p af "), "ICCMA must start with 'p af'");
        let n: usize = header
            .strip_prefix("p af ")
            .unwrap()
            .trim()
            .parse()
            .expect("argument count");
        assert_eq!(n, af.arguments.len());

        for line in &lines[1..] {
            let parts: Vec<usize> = line
                .split_whitespace()
                .map(|p| p.parse().expect("1-based ID"))
                .collect();
            assert_eq!(parts.len(), 2);
            assert!(parts[0] >= 1, "ICCMA uses 1-based indexing");
            assert!(parts[1] >= 1, "ICCMA uses 1-based indexing");
        }
    }

    #[test]
    fn aspartix_round_trip() {
        let (af, _store) = small_af();
        let apx = af.to_aspartix();

        let (parsed_af, name_map) = AbstractFramework::from_aspartix(&apx).unwrap();

        assert_eq!(parsed_af.arguments.len(), af.arguments.len());
        assert_eq!(parsed_af.defeats.len(), af.defeats.len());

        let mut orig_edges: BTreeSet<(usize, usize)> = BTreeSet::new();
        for (a, b) in &af.defeats {
            orig_edges.insert((a.0, b.0));
        }

        let id_map: HashMap<ArgumentId, usize> = name_map
            .iter()
            .map(|(name, &id)| {
                let orig_idx: usize = name.strip_prefix('a').unwrap().parse().unwrap();
                (id, orig_idx)
            })
            .collect();

        let mut parsed_edges: BTreeSet<(usize, usize)> = BTreeSet::new();
        for (a, b) in &parsed_af.defeats {
            parsed_edges.insert((id_map[a], id_map[b]));
        }

        assert_eq!(
            orig_edges, parsed_edges,
            "ASPARTIX round-trip preserves topology"
        );
    }

    #[test]
    fn dot_escapes_quotes() {
        let (system, _) = AspicSystemBuilder::new()
            .ordinary_premise(Formula::prop("has\"quote"))
            .build();

        let pipeline = AspicPipeline::classical(system, Box::new(EqualOrdering));
        let result = pipeline.evaluate(Semantics::Grounded).unwrap();

        let defeats = compute_defeats(&result.attacks, &result.store, &EqualOrdering);
        let af = AbstractFramework::from_defeats(&result.store, &defeats);
        let dot = af.to_dot(&result.store);

        assert!(
            dot.contains("\\\""),
            "quotes in conclusions should be escaped in DOT output"
        );
        assert!(
            !dot.contains("has\"quote"),
            "raw unescaped quote should not appear"
        );
    }

    #[test]
    fn iccma_empty_framework() {
        let af = AbstractFramework::from_defeats(&ArgumentStore::default(), &[]);
        let iccma = af.to_iccma();
        assert_eq!(iccma.trim(), "p af 0", "empty AF produces 'p af 0'");
    }

    #[test]
    fn tgf_empty_framework() {
        let af = AbstractFramework::from_defeats(&ArgumentStore::default(), &[]);
        let tgf = af.to_tgf();
        assert_eq!(tgf.trim(), "#", "empty AF produces only '#' separator");
    }
}

// ---
// Error handling
// ---
mod error_handling {
    use super::*;

    #[test]
    fn aspartix_parse_bad_syntax() {
        let result = AbstractFramework::from_aspartix("att(A,).");
        assert!(
            matches!(
                result,
                Err(AspicError::Solver(SolverError::AspartixParse(_)))
            ),
            "bad syntax should produce AspartixParse error"
        );
    }

    #[test]
    fn aspartix_parse_undefined_argument() {
        let result = AbstractFramework::from_aspartix("arg(A).\natt(A,B).\n");
        match &result {
            Err(AspicError::Solver(SolverError::AspartixParse(msg))) => {
                assert!(
                    msg.contains("undefined argument"),
                    "error should mention undefined argument, got: {msg}"
                );
            }
            _ => panic!("expected AspartixParse error with 'undefined argument', got {result:?}"),
        }
    }

    #[test]
    fn error_display_messages() {
        let errors: Vec<AspicError> = vec![
            SolverError::AspartixParse("test error".into()).into(),
            SolverError::NotFound("/usr/bin/clingo".into()).into(),
            SolverError::Failed("solver crashed".into()).into(),
        ];

        for err in &errors {
            let msg = err.to_string();
            assert!(!msg.is_empty(), "error message should not be empty");
        }

        assert!(
            AspicError::from(SolverError::NotFound("/usr/bin/clingo".into()))
                .to_string()
                .contains("/usr/bin/clingo"),
            "ExternalSolverNotFound message should contain path"
        );
    }

    #[test]
    fn all_variants_constructable() {
        let _exhaustive: Vec<AspicError> = vec![
            AspicError::PipelineStageError {
                stage: PipelineStage::Grounding,
                source: Box::new(SolverError::Failed(String::new()).into()),
            },
            SolverError::AspartixParse(String::new()).into(),
            SolverError::NotFound(String::new()).into(),
            SolverError::Failed(String::new()).into(),
            SolverError::PowersetLimitExceeded {
                count: 64,
                limit: 64,
            }
            .into(),
            SerialError::UnknownContrarinessRelation("unknown".into()).into(),
            SerialError::UnknownPremiseKind("unknown".into()).into(),
        ];
    }
}

// ---
// Property tests
// ---

#[cfg(any(feature = "json", feature = "toml-ser"))]
fn make_atom(i: usize) -> Formula {
    Formula::Lit(Literal::Pos(Atom {
        predicate: format!("p{i}"),
        terms: vec![],
    }))
}

#[cfg(any(feature = "json", feature = "toml-ser"))]
fn arb_small_system() -> impl Strategy<Value = AspicSystem> {
    let n_atoms = 2..=3usize;
    let n_defeasible = 0..=2usize;

    (n_atoms, n_defeasible)
        .prop_flat_map(|(na, nd)| {
            let atoms: Vec<Formula> = (0..na).map(make_atom).collect();
            let n_all = atoms.len();

            let axiom_idx =
                proptest::sample::subsequence((0..na).collect::<Vec<_>>(), 1..=1usize.min(na));
            let ord_idx = proptest::sample::subsequence((0..na).collect::<Vec<_>>(), 1..=na);
            let def_rules = proptest::collection::vec(
                (
                    proptest::sample::subsequence((0..n_all).collect::<Vec<_>>(), 1..=2),
                    0..n_all,
                ),
                0..=nd,
            );

            (Just(atoms), axiom_idx, ord_idx, def_rules)
        })
        .prop_filter_map("valid small system", |(atoms, ax_idx, ord_idx, def_raw)| {
            let mut builder = AspicSystemBuilder::new().with_classical_negation();

            for &i in &ax_idx {
                builder = builder.axiom(atoms[i].clone());
            }
            for &i in &ord_idx {
                if !ax_idx.contains(&i) {
                    builder = builder.ordinary_premise(atoms[i].clone());
                }
            }

            for (k, (ant_idx, cons_idx)) in def_raw.into_iter().enumerate() {
                if ant_idx.is_empty() {
                    continue;
                }
                let ant: Vec<Formula> = ant_idx.iter().map(|&i| atoms[i].clone()).collect();
                let cons = atoms[cons_idx].classical_negation();
                let id = format!("d{k}");
                builder = builder.defeasible_rule(&id, ant, cons);
            }

            let (system, _) = builder.build();
            if system.knowledge_base.premises.is_empty() {
                return None;
            }
            Some(system)
        })
}

#[cfg(feature = "json")]
proptest! {
    #![proptest_config(ProptestConfig::with_cases(32))]

    #[test]
    fn json_round_trip_property(system in arb_small_system()) {
        let ser = SerializableSystem::from_system(&system);
        let json = ser.to_json().expect("JSON serialization");
        let restored = SerializableSystem::from_json(&json)
            .expect("JSON deserialization")
            .to_system()
            .unwrap();

        let orig_result =
            AspicPipeline::classical(system, Box::new(EqualOrdering))
                .evaluate(Semantics::Grounded)
                .unwrap();
        let rest_result =
            AspicPipeline::classical(restored, Box::new(EqualOrdering))
                .evaluate(Semantics::Grounded)
                .unwrap();

        let orig_conc = conclusions_in(&orig_result.extensions[0], &orig_result.store);
        let rest_conc = conclusions_in(&rest_result.extensions[0], &rest_result.store);
        prop_assert_eq!(orig_conc, rest_conc);
    }
}

#[cfg(all(feature = "json", feature = "toml-ser"))]
proptest! {
    #![proptest_config(ProptestConfig::with_cases(32))]

    #[test]
    fn toml_json_equivalence_property(system in arb_small_system()) {
        let ser = SerializableSystem::from_system(&system);

        let via_json = SerializableSystem::from_json(&ser.to_json().unwrap())
            .unwrap()
            .to_system()
            .unwrap();
        let via_toml = SerializableSystem::from_toml(&ser.to_toml().unwrap())
            .unwrap()
            .to_system()
            .unwrap();

        let json_result =
            AspicPipeline::classical(via_json, Box::new(EqualOrdering))
                .evaluate(Semantics::Grounded)
                .unwrap();
        let toml_result =
            AspicPipeline::classical(via_toml, Box::new(EqualOrdering))
                .evaluate(Semantics::Grounded)
                .unwrap();

        let json_conc = conclusions_in(&json_result.extensions[0], &json_result.store);
        let toml_conc = conclusions_in(&toml_result.extensions[0], &toml_result.store);
        prop_assert_eq!(json_conc, toml_conc);
    }
}

#[cfg(feature = "json")]
#[test]
fn unknown_contrariness_relation_returns_error() {
    let json = r#"{
        "premises": [],
        "strict_rules": [],
        "defeasible_rules": [],
        "contrariness": [
            {"target": {"Lit": {"Pos": {"predicate": "p", "terms": []}}},
             "attacker": {"Lit": {"Pos": {"predicate": "q", "terms": []}}},
             "relation": "contrray"}
        ],
        "classical_negation": false
    }"#;
    let sys = SerializableSystem::from_json(json).unwrap();
    let err = sys.to_system().unwrap_err();
    assert!(
        format!("{err}").contains("unknown contrariness relation"),
        "expected UnknownContrarinessRelation, got: {err}"
    );
}

#[cfg(feature = "json")]
#[test]
fn unknown_premise_kind_returns_error() {
    let json = r#"{
        "premises": [
            {"formula": {"Lit": {"Pos": {"predicate": "p", "terms": []}}},
             "kind": "axom"}
        ],
        "strict_rules": [],
        "defeasible_rules": [],
        "contrariness": [],
        "classical_negation": false
    }"#;
    let sys = SerializableSystem::from_json(json).unwrap();
    let err = sys.to_system().unwrap_err();
    assert!(
        format!("{err}").contains("unknown premise kind"),
        "expected UnknownPremiseKind, got: {err}"
    );
}
