//use crate::manager::{Manager, TripleUpdate};
use crate::reasoner::*;

use std::io::Error;

const RDFS_SUBCLASSOF: &str = "http://www.w3.org/2000/01/rdf-schema#subClassOf";
const RDFS_DOMAIN: &str = "http://www.w3.org/2000/01/rdf-schema#domain";
const RDFS_RANGE: &str = "http://www.w3.org/2000/01/rdf-schema#range";
const RDFS_SUBPROP: &str = "http://www.w3.org/2000/01/rdf-schema#subPropertyOf";
const RDF_TYPE: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#type";
const RDF_FIRST: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#first";
const RDF_REST: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#rest";
const RDF_NIL: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#nil";
const RDF_PROPERTY: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#Property";
const RDF_XML_LITERAL: &str = "http://www.w3.org/1999/02/22-rdf-syntax-ns#XMLLiteral";
const RDFS_MEMBER: &str = "http://www.w3.org/2000/01/rdf-schema#member";
const RDFS_CONTAINER_MEMBERSHIP_PROPERTY: &str =
    "http://www.w3.org/2000/01/rdf-schema#ContainerMembershipProperty";
const XSD_STRING: &str = "http://www.w3.org/2001/XMLSchema#string";
const XSD_INTEGER: &str = "http://www.w3.org/2001/XMLSchema#integer";
const XSD_INT: &str = "http://www.w3.org/2001/XMLSchema#int";
const OWL_SAMEAS: &str = "http://www.w3.org/2002/07/owl#sameAs";
const OWL_EQUIVALENTCLASS: &str = "http://www.w3.org/2002/07/owl#equivalentClass";
const OWL_HASVALUE: &str = "http://www.w3.org/2002/07/owl#hasValue";
const OWL_ALLVALUESFROM: &str = "http://www.w3.org/2002/07/owl#allValuesFrom";
const OWL_SOMEVALUESFROM: &str = "http://www.w3.org/2002/07/owl#someValuesFrom";
const OWL_ONPROPERTY: &str = "http://www.w3.org/2002/07/owl#onProperty";
const OWL_INVERSEOF: &str = "http://www.w3.org/2002/07/owl#inverseOf";
const OWL_SYMMETRICPROP: &str = "http://www.w3.org/2002/07/owl#SymmetricProperty";
const OWL_EQUIVPROP: &str = "http://www.w3.org/2002/07/owl#equivalentProperty";
const OWL_FUNCPROP: &str = "http://www.w3.org/2002/07/owl#FunctionalProperty";
const OWL_INVFUNCPROP: &str = "http://www.w3.org/2002/07/owl#InverseFunctionalProperty";
const OWL_TRANSPROP: &str = "http://www.w3.org/2002/07/owl#TransitiveProperty";
const OWL_INTERSECTION: &str = "http://www.w3.org/2002/07/owl#intersectionOf";
const OWL_UNION: &str = "http://www.w3.org/2002/07/owl#unionOf";
const OWL_CLASS: &str = "http://www.w3.org/2002/07/owl#Class";
const OWL_THING: &str = "http://www.w3.org/2002/07/owl#Thing";
const OWL_NOTHING: &str = "http://www.w3.org/2002/07/owl#Nothing";
const OWL_COMPLEMENT: &str = "http://www.w3.org/2002/07/owl#complementOf";
const OWL_ASYMMETRICPROP: &str = "http://www.w3.org/2002/07/owl#AsymmetricProperty";
const OWL_IRREFLEXIVEPROP: &str = "http://www.w3.org/2002/07/owl#IrreflexiveProperty";

macro_rules! wrap {
    ($t:expr) => {
        format!("<{}>", $t)
    };
}

#[test]
fn test_make_reasoner() -> Result<(), Error> {
    let _r = Reasoner::new();
    Ok(())
}

#[test]
fn test_load_file_ttl() -> crate::error::Result<()> {
    let mut r = Reasoner::new();
    r.load_file("../example_models/ontologies/rdfs.ttl")
}

#[test]
fn test_load_file_n3() -> crate::error::Result<()> {
    let mut r = Reasoner::new();
    r.load_file("../example_models/ontologies/Brick.n3")
}

#[test]
#[ignore]
fn test_eq_ref() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![("a", "b", "c")];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&("a".to_string(), wrap!(OWL_SAMEAS), "a".to_string())));
    assert!(res.contains(&("b".to_string(), wrap!(OWL_SAMEAS), "b".to_string())));
    assert!(res.contains(&("c".to_string(), wrap!(OWL_SAMEAS), "c".to_string())));
    Ok(())
}

#[test]
fn test_eq_sym() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![("urn:x", OWL_SAMEAS, "urn:y")];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(OWL_SAMEAS),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_eq_trans() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_SAMEAS, "urn:y"),
        ("urn:y", OWL_SAMEAS, "urn:z"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        wrap!(OWL_SAMEAS),
        "<urn:z>".to_string()
    )));
    Ok(())
}

#[test]
fn test_eq_rep_s() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:s1", OWL_SAMEAS, "urn:s2"),
        ("urn:s1", "urn:p", "urn:o"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:s2>".to_string(),
        "<urn:p>".to_string(),
        "<urn:o>".to_string()
    )));
    Ok(())
}

#[test]
fn test_eq_rep_p() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p1", OWL_SAMEAS, "urn:p2"),
        ("urn:s", "urn:p1", "urn:o"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:s>".to_string(),
        "<urn:p2>".to_string(),
        "<urn:o>".to_string()
    )));
    Ok(())
}

#[test]
fn test_eq_rep_o() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:o1", OWL_SAMEAS, "urn:o2"),
        ("urn:s", "urn:p", "urn:o1"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:s>".to_string(),
        "<urn:p>".to_string(),
        "<urn:o2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cax_sco() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:Class2", RDFS_SUBCLASSOF, "urn:Class1"),
        ("urn:a", RDF_TYPE, "urn:Class2"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let _res = r.get_triples();
    let res: Vec<(String, String, String)> = _res
        .iter()
        .map(|t| {
            (
                t.subject.to_string(),
                t.predicate.to_string(),
                t.object.to_string(),
            )
        })
        .collect();
    // let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class1>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cax_eqc1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:Class1", OWL_EQUIVALENTCLASS, "urn:Class2"),
        ("urn:a", RDF_TYPE, "urn:Class1"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cax_eqc2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:Class1", OWL_EQUIVALENTCLASS, "urn:Class2"),
        ("urn:a", RDF_TYPE, "urn:Class2"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class1>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cax_eqc_chain_1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:Class1", OWL_EQUIVALENTCLASS, "urn:Class2"),
        ("urn:Class2", OWL_EQUIVALENTCLASS, "urn:Class3"),
        ("urn:Class3", OWL_EQUIVALENTCLASS, "urn:Class4"),
        ("urn:Class4", OWL_EQUIVALENTCLASS, "urn:Class5"),
        ("urn:Class5", OWL_EQUIVALENTCLASS, "urn:Class6"),
        ("urn:a", RDF_TYPE, "urn:Class1"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class3>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class4>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class5>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class6>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cax_eqc_chain_2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:Class1", OWL_EQUIVALENTCLASS, "urn:Class2"),
        ("urn:Class2", OWL_EQUIVALENTCLASS, "urn:Class3"),
        ("urn:Class3", OWL_EQUIVALENTCLASS, "urn:Class4"),
        ("urn:Class4", OWL_EQUIVALENTCLASS, "urn:Class5"),
        ("urn:Class5", OWL_EQUIVALENTCLASS, "urn:Class6"),
        ("urn:a", RDF_TYPE, "urn:Class6"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class1>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class3>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class4>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:a>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:Class5>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_fp() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:PRED", RDF_TYPE, OWL_FUNCPROP),
        ("urn:SUB", "urn:PRED", "urn:OBJECT_1"),
        ("urn:SUB", "urn:PRED", "urn:OBJECT_2"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:OBJECT_1>".to_string(),
        wrap!(OWL_SAMEAS),
        "<urn:OBJECT_2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_fp_2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:PRED", RDF_TYPE, OWL_FUNCPROP),
        ("urn:SUB", "urn:PRED", "urn:OBJECT_1"),
        ("urn:SUB1", "urn:PRED", "urn:OBJECT_2"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(!res.contains(&(
        "<urn:OBJECT_1>".to_string(),
        wrap!(OWL_SAMEAS),
        "<urn:OBJECT_2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_ifp() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:PRED", RDF_TYPE, OWL_INVFUNCPROP),
        ("urn:SUB_1", "urn:PRED", "urn:OBJECT"),
        ("urn:SUB_2", "urn:PRED", "urn:OBJECT"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:SUB_1>".to_string(),
        wrap!(OWL_SAMEAS),
        "<urn:SUB_2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_spo1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p1", RDFS_SUBPROP, "urn:p2"),
        ("urn:x", "urn:p1", "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        "<urn:p2>".to_string(),
        "<urn:y>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_inv1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p1", OWL_INVERSEOF, "urn:p2"),
        ("urn:x", "urn:p1", "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        "<urn:p2>".to_string(),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_inv2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p1", OWL_INVERSEOF, "urn:p2"),
        ("urn:y", "urn:p2", "urn:x"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        "<urn:p1>".to_string(),
        "<urn:y>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_symp() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p", RDF_TYPE, OWL_SYMMETRICPROP),
        ("urn:x", "urn:p", "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        "<urn:p>".to_string(),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_trp() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p", RDF_TYPE, OWL_TRANSPROP),
        ("urn:x", "urn:p", "urn:y"),
        ("urn:y", "urn:p", "urn:z"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        "<urn:p>".to_string(),
        "<urn:z>".to_string()
    )));
    Ok(())
}

#[test]
fn test_prp_eqp1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p1", OWL_EQUIVPROP, "urn:p2"),
        ("urn:x", "urn:p1", "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        "<urn:p2>".to_string(),
        "<urn:y>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_thing_nothing() -> Result<(), String> {
    let mut r = Reasoner::new();
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(wrap!(OWL_THING), wrap!(RDF_TYPE), wrap!(OWL_CLASS))));
    assert!(res.contains(&(wrap!(OWL_NOTHING), wrap!(RDF_TYPE), wrap!(OWL_CLASS))));
    Ok(())
}

#[test]
fn test_cls_hv1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_HASVALUE, "urn:y"),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:u", RDF_TYPE, "urn:x"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:u>".to_string(),
        "<urn:p>".to_string(),
        "<urn:y>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_hv2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_HASVALUE, "urn:y"),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:u", "urn:p", "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:u>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_avf() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_ALLVALUESFROM, "urn:y"),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:u", RDF_TYPE, "urn:x"),
        ("urn:u", "urn:p", "urn:v"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:v>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:y>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_svf1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_SOMEVALUESFROM, "urn:y"),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:u", "urn:p", "urn:v"),
        ("urn:v", RDF_TYPE, "urn:y"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:u>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_svf2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:x", OWL_SOMEVALUESFROM, OWL_THING),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:u", "urn:p", "urn:v"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:u>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:x>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_int1() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:c", OWL_INTERSECTION, "urn:x"),
        ("urn:x", RDF_FIRST, "urn:c1"),
        ("urn:x", RDF_REST, "urn:z2"),
        ("urn:z2", RDF_FIRST, "urn:c2"),
        ("urn:z2", RDF_REST, "urn:z3"),
        ("urn:z3", RDF_FIRST, "urn:c3"),
        ("urn:z3", RDF_REST, RDF_NIL),
        ("urn:y", RDF_TYPE, "urn:c1"),
        ("urn:y", RDF_TYPE, "urn:c2"),
        ("urn:y", RDF_TYPE, "urn:c3"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_int2() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:c", OWL_INTERSECTION, "urn:x"),
        ("urn:x", RDF_FIRST, "urn:c1"),
        ("urn:x", RDF_REST, "urn:z2"),
        ("urn:z2", RDF_FIRST, "urn:c2"),
        ("urn:z2", RDF_REST, "urn:z3"),
        ("urn:z3", RDF_FIRST, "urn:c3"),
        ("urn:z3", RDF_REST, RDF_NIL),
        ("urn:y", RDF_TYPE, "urn:c"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c1>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c3>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_int2_withequivalent() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:c", OWL_INTERSECTION, "urn:x"),
        ("urn:x", RDF_FIRST, "urn:c1"),
        ("urn:x", RDF_REST, "urn:z2"),
        ("urn:z2", RDF_FIRST, "urn:c2"),
        ("urn:z2", RDF_REST, "urn:z3"),
        ("urn:z3", RDF_FIRST, "urn:c3"),
        ("urn:z3", RDF_REST, RDF_NIL),
        ("urn:y", RDF_TYPE, "urn:c"),
        ("urn:c", OWL_EQUIVALENTCLASS, "urn:C"),
        ("urn:C", OWL_INTERSECTION, "urn:X"),
        ("urn:X", RDF_FIRST, "urn:C1"),
        ("urn:X", RDF_REST, "urn:Z2"),
        ("urn:Z2", RDF_FIRST, "urn:C2"),
        ("urn:Z2", RDF_REST, "urn:Z3"),
        ("urn:Z3", RDF_FIRST, "urn:C3"),
        ("urn:Z3", RDF_REST, RDF_NIL),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c1>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c3>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:C1>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:C2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:y>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:C3>".to_string()
    )));
    Ok(())
}

#[test]
fn test_cls_int1_withhasvalue() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:intersection_class", OWL_INTERSECTION, "urn:x"),
        ("urn:x", RDF_FIRST, "urn:c1"),
        ("urn:x", RDF_REST, "urn:z2"),
        ("urn:z2", RDF_FIRST, "urn:c2"),
        ("urn:z2", RDF_REST, RDF_NIL),
        ("urn:c1", OWL_HASVALUE, "urn:c1p_value"),
        ("urn:c1", OWL_ONPROPERTY, "urn:c1p"),
        ("urn:c2", OWL_HASVALUE, "urn:c2p_value"),
        ("urn:c2", OWL_ONPROPERTY, "urn:c2p"),
        ("urn:inst", "urn:c1p", "urn:c1p_value"),
        ("urn:inst", "urn:c2p", "urn:c2p_value"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&(
        "<urn:inst>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c1>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:inst>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c2>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:inst>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:intersection_class>".to_string()
    )));
    Ok(())
}

#[test]
fn test_complementof() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:c", OWL_EQUIVALENTCLASS, "urn:c2"),
        ("urn:c2", OWL_COMPLEMENT, "urn:x"),
        ("urn:x", OWL_HASVALUE, "urn:v"),
        ("urn:x", OWL_ONPROPERTY, "urn:p"),
        ("urn:inst1", "urn:p", "urn:v"),
        ("urn:inst2", "urn:p", "urn:v2"),
        ("urn:x", RDF_TYPE, OWL_CLASS),
        ("urn:c", RDF_TYPE, OWL_CLASS),
        ("urn:c2", RDF_TYPE, OWL_CLASS),
        ("urn:inst2", RDF_TYPE, OWL_THING),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    assert!(res.contains(&("<urn:inst1>".to_string(), wrap!(RDF_TYPE), wrap!(OWL_THING))));
    assert!(res.contains(&(
        "<urn:inst1>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:x>".to_string()
    )));
    assert!(!res.contains(&(
        "<urn:inst1>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c>".to_string()
    )));
    assert!(!res.contains(&(
        "<urn:inst1>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c2>".to_string()
    )));
    // Under OWL 2 RL (open world), we do not materialize membership in
    // the complement class merely because a different value is present.
    // Therefore, inst2 should NOT be inferred as type c2.
    assert!(!res.contains(&(
        "<urn:inst2>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:c2>".to_string()
    )));
    Ok(())
}

#[test]
fn test_error_asymmetric() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p", RDF_TYPE, OWL_ASYMMETRICPROP),
        ("urn:x", "urn:p", "urn:y"),
        ("urn:y", "urn:p", "urn:x"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    for i in res.iter() {
        let (s, p, o) = i;
        println!("{} {} {}", s, p, o);
    }
    // assert!(res.errors.len() > 0);
    Ok(())
}

#[test]
fn test_prp_irp_violation() -> Result<(), String> {
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:p", RDF_TYPE, OWL_IRREFLEXIVEPROP),
        ("urn:x", "urn:p", "urn:x"),
    ];
    r.load_triples_str(trips);
    r.reason();
    // Expect an irreflexive property diagnostic
    let has_irp = r
        .errors()
        .iter()
        .any(|e| e.code() == "OWLRL.PRP_IRP" || e.rule() == "prp-irp");
    assert!(has_irp, "expected PRP_IRP diagnostic");
    Ok(())
}

#[test]
fn test_cax_dw() -> Result<(), String> {
    // If A disjointWith B and an instance is typed as both,
    // the reasoner should record a cax-dw error (no new triples are asserted).
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", RDF_TYPE, OWL_CLASS),
        ("urn:B", RDF_TYPE, OWL_CLASS),
        ("urn:A", "http://www.w3.org/2002/07/owl#disjointWith", "urn:B"),
        ("urn:i", RDF_TYPE, "urn:A"),
        ("urn:i", RDF_TYPE, "urn:B"),
    ];
    r.load_triples_str(trips);
    r.reason();
    // Expect at least one disjointness violation recorded
    assert!(r.errors().iter().any(|e| e.to_string().contains("cax-dw")) || r.errors().len() > 0);
    Ok(())
}

#[test]
fn test_rdfs11() -> Result<(), String> {
    // Basic transitivity: A subClassOf B, B subClassOf C => A subClassOf C
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:C>".to_string()
    )));
    Ok(())
}

#[test]
fn test_rdfs11_long_chain() -> Result<(), String> {
    // 4-level chain: A subClassOf B subClassOf C subClassOf D
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
        ("urn:C", RDFS_SUBCLASSOF, "urn:D"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    // A subClassOf C (one hop)
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:C>".to_string()
    )));
    // A subClassOf D (two hops)
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:D>".to_string()
    )));
    // B subClassOf D (one hop)
    assert!(res.contains(&(
        "<urn:B>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:D>".to_string()
    )));
    Ok(())
}

#[test]
fn test_rdfs11_with_instances() -> Result<(), String> {
    // Transitivity + instance propagation together
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    // TBox: A subClassOf C (rdfs11)
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:C>".to_string()
    )));
    // ABox: x rdf:type C (cax-sco)
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:C>".to_string()
    )));
    Ok(())
}

#[test]
fn test_scm_eqc_basic() -> Result<(), String> {
    // equivalentClass implies subClassOf in both directions
    let mut r = Reasoner::new();
    let trips = vec![("urn:A", OWL_EQUIVALENTCLASS, "urn:B")];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:B>".to_string()
    )));
    assert!(res.contains(&(
        "<urn:B>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:A>".to_string()
    )));
    Ok(())
}

#[test]
fn test_equivalentclass_transitivity() -> Result<(), String> {
    // A eqClass B, B eqClass C
    // => A subClassOf C and C subClassOf A (transitive via rdfs11)
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", OWL_EQUIVALENTCLASS, "urn:B"),
        ("urn:B", OWL_EQUIVALENTCLASS, "urn:C"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    // A subClassOf C (via scm-eqc + rdfs11)
    assert!(res.contains(&(
        "<urn:A>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:C>".to_string()
    )));
    // C subClassOf A (via scm-eqc + rdfs11)
    assert!(res.contains(&(
        "<urn:C>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:A>".to_string()
    )));
    Ok(())
}

#[test]
fn test_subclassof_through_equivalentclass() -> Result<(), String> {
    // A eqClass B, C subClassOf B => C subClassOf A
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", OWL_EQUIVALENTCLASS, "urn:B"),
        ("urn:C", RDFS_SUBCLASSOF, "urn:B"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:C>".to_string(),
        wrap!(RDFS_SUBCLASSOF),
        "<urn:A>".to_string()
    )));
    Ok(())
}

#[test]
fn test_scm_eqc_with_instances() -> Result<(), String> {
    // A eqClass B, C subClassOf B, x rdf:type C => x rdf:type A
    let mut r = Reasoner::new();
    let trips = vec![
        ("urn:A", OWL_EQUIVALENTCLASS, "urn:B"),
        ("urn:C", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:C"),
    ];
    r.load_triples_str(trips);
    r.reason();
    let res = r.get_triples_string();
    assert!(res.contains(&(
        "<urn:x>".to_string(),
        wrap!(RDF_TYPE),
        "<urn:A>".to_string()
    )));
    Ok(())
}

// ==================== RDFS container/datatype entailment tests ====================
//
// Tests for the container-membership-property axiomatisation and the
// datatype well-formedness / range-clash diagnostics introduced in
// commit 8f866a5 ("reasonable: add rdfs container/datatype entailment fixes
// for W3C tests").
//
// W3C RDF Semantics test cross-reference:
//   https://github.com/w3c/rdf-tests/tree/main/rdf/rdf11/rdf-mt
//   - rdfms-seq-representation-test002 / -test003 / -test004
//   - rdfs-container-membership-superProperty-test001
//   - xmlsch-02-whitespace-facet-1 / -2 / -4
//   - rdfms-xmllang-test007a / b / c
//   - pfps-10-non-well-formed-literal-1

/// Build an oxrdf Triple with a typed literal object.
fn typed_literal_triple(s: &str, p: &str, value: &str, datatype: &str) -> oxrdf::Triple {
    use crate::common::make_triple;
    make_triple(
        oxrdf::Term::NamedNode(oxrdf::NamedNode::new(s).unwrap()),
        oxrdf::Term::NamedNode(oxrdf::NamedNode::new(p).unwrap()),
        oxrdf::Term::Literal(oxrdf::Literal::new_typed_literal(
            value,
            oxrdf::NamedNode::new(datatype).unwrap(),
        )),
    )
    .unwrap()
}

/// Build an oxrdf Triple with a language-tagged literal object.
fn lang_literal_triple(s: &str, p: &str, value: &str, language: &str) -> oxrdf::Triple {
    use crate::common::make_triple;
    make_triple(
        oxrdf::Term::NamedNode(oxrdf::NamedNode::new(s).unwrap()),
        oxrdf::Term::NamedNode(oxrdf::NamedNode::new(p).unwrap()),
        oxrdf::Term::Literal(oxrdf::Literal::new_language_tagged_literal_unchecked(
            value, language,
        )),
    )
    .unwrap()
}

#[test]
fn test_rdfs_container_membership_axioms() -> Result<(), String> {
    // W3C rdf-mt: rdfms-seq-representation-test002 and test004.
    // Any triple using rdf:_N (N>0) as predicate must axiomatically entail:
    //   rdf:_N rdf:type rdfs:ContainerMembershipProperty
    //   rdf:_N rdfs:subPropertyOf rdfs:member
    //   rdf:_N rdf:type rdf:Property
    let mut r = Reasoner::new();
    r.load_triples_str(vec![(
        "http://example.org/foo",
        "http://www.w3.org/1999/02/22-rdf-syntax-ns#_1",
        "http://example.org/bar",
    )]);
    r.reason();
    let res = r.get_triples_string();
    let rdf_n1 = "<http://www.w3.org/1999/02/22-rdf-syntax-ns#_1>".to_string();
    // test002 conclusion: rdf:_1 rdf:type rdfs:ContainerMembershipProperty
    assert!(
        res.contains(&(
            rdf_n1.clone(),
            wrap!(RDF_TYPE),
            wrap!(RDFS_CONTAINER_MEMBERSHIP_PROPERTY)
        )),
        "expected rdf:_1 rdf:type rdfs:ContainerMembershipProperty (W3C rdfms-seq-representation-test002)"
    );
    // test004 conclusion: rdf:_1 rdfs:subPropertyOf rdfs:member
    assert!(
        res.contains(&(rdf_n1.clone(), wrap!(RDFS_SUBPROP), wrap!(RDFS_MEMBER))),
        "expected rdf:_1 rdfs:subPropertyOf rdfs:member (W3C rdfms-seq-representation-test004)"
    );
    // RDF axiomatic: rdf:_1 rdf:type rdf:Property
    assert!(
        res.contains(&(rdf_n1, wrap!(RDF_TYPE), wrap!(RDF_PROPERTY))),
        "expected rdf:_1 rdf:type rdf:Property (RDF axiomatic triple)"
    );
    Ok(())
}

#[test]
fn test_rdfs_container_membership_entails_member() -> Result<(), String> {
    // W3C rdf-mt: rdfms-seq-representation-test003.
    // <a> rdf:_1 <b>  =>  <a> rdfs:member <b>
    // (via rdf:_1 rdfs:subPropertyOf rdfs:member and prp-spo1)
    let mut r = Reasoner::new();
    r.load_triples_str(vec![(
        "http://example.org/a",
        "http://www.w3.org/1999/02/22-rdf-syntax-ns#_1",
        "http://example.org/b",
    )]);
    r.reason();
    let res = r.get_triples_string();
    assert!(
        res.contains(&(
            "<http://example.org/a>".to_string(),
            wrap!(RDFS_MEMBER),
            "<http://example.org/b>".to_string()
        )),
        "expected <a> rdfs:member <b> (W3C rdfms-seq-representation-test003)"
    );
    Ok(())
}

#[test]
fn test_rdfs_container_membership_multiple_indices() -> Result<(), String> {
    // Axioms must fire for every distinct rdf:_N (N>0) predicate observed.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_1", "urn:o1"),
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_2", "urn:o2"),
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_42", "urn:o42"),
    ]);
    r.reason();
    let res = r.get_triples_string();
    for n in &[1u32, 2, 42] {
        let rdf_n = format!("<http://www.w3.org/1999/02/22-rdf-syntax-ns#_{}>", n);
        assert!(
            res.contains(&(
                rdf_n.clone(),
                wrap!(RDFS_SUBPROP),
                wrap!(RDFS_MEMBER)
            )),
            "missing rdf:_{} rdfs:subPropertyOf rdfs:member axiom",
            n
        );
        let o = format!("<urn:o{}>", n);
        assert!(
            res.contains(&("<urn:s>".to_string(), wrap!(RDFS_MEMBER), o)),
            "missing urn:s rdfs:member urn:o{} entailment",
            n
        );
    }
    Ok(())
}

#[test]
fn test_rdfs_container_membership_ignores_non_numeric_and_zero() -> Result<(), String> {
    // rdf:_abc, rdf:_0, and bare rdf:_ are NOT container membership properties.
    // (The detector requires a strictly-positive integer suffix.)
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_abc", "urn:o"),
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_0", "urn:o2"),
        ("urn:s", "http://www.w3.org/1999/02/22-rdf-syntax-ns#_", "urn:o3"),
    ]);
    r.reason();
    let res = r.get_triples_string();
    for suffix in &["_abc", "_0", "_"] {
        let p = format!("<http://www.w3.org/1999/02/22-rdf-syntax-ns#{}>", suffix);
        assert!(
            !res.contains(&(
                p.clone(),
                wrap!(RDF_TYPE),
                wrap!(RDFS_CONTAINER_MEMBERSHIP_PROPERTY)
            )),
            "rdf:{} should not be a ContainerMembershipProperty",
            suffix
        );
        assert!(
            !res.contains(&(p, wrap!(RDFS_SUBPROP), wrap!(RDFS_MEMBER))),
            "rdf:{} should not be subPropertyOf rdfs:member",
            suffix
        );
    }
    Ok(())
}

#[test]
fn test_rdfs_container_membership_super_property_negative() -> Result<(), String> {
    // W3C rdf-mt: rdfs-container-membership-superProperty-test001 (NegativeEntailmentTest).
    // <s> rdfs:member <o> does NOT entail <s> rdf:_N <o> for any N.
    // i.e. the rule fires only in the direction rdf:_N -> rdfs:member.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![(
        "http://example/stuff#something",
        RDFS_MEMBER,
        "http://example/stuff#somethingElse",
    )]);
    r.reason();
    let res = r.get_triples_string();
    // No rdf:_N triple should appear with these endpoints.
    for n in 1..5 {
        let rdf_n = format!("<http://www.w3.org/1999/02/22-rdf-syntax-ns#_{}>", n);
        assert!(
            !res.contains(&(
                "<http://example/stuff#something>".to_string(),
                rdf_n.clone(),
                "<http://example/stuff#somethingElse>".to_string()
            )),
            "rdfs:member should not entail rdf:_{} (W3C rdfs-container-membership-superProperty-test001)",
            n
        );
    }
    Ok(())
}

#[test]
fn test_rdfs_datatype_ill_formed_xsd_int_with_whitespace() -> Result<(), String> {
    // W3C rdf-mt: xmlsch-02-whitespace-facet-2 / -4.
    // " 3 "^^xsd:int has leading/trailing whitespace and is ill-formed.
    // The reasoner should record an rdfs-datatype diagnostic.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "http://www.example.org/a",
        "http://example.org/prop",
        " 3 ",
        XSD_INT,
    )]);
    r.reason();
    assert!(
        r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "expected rdfs-datatype diagnostic for ill-formed xsd:int literal \" 3 \" (W3C xmlsch-02-whitespace-facet-2/-4)"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_well_formed_xsd_int_no_error() -> Result<(), String> {
    // W3C rdf-mt: xmlsch-02-whitespace-facet-1 premise (test001.ttl).
    // "3"^^xsd:int is well-formed; no rdfs-datatype diagnostic should fire.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "http://www.example.org/a",
        "http://example.org/prop",
        "3",
        XSD_INT,
    )]);
    r.reason();
    assert!(
        !r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "no rdfs-datatype diagnostic should be raised for well-formed \"3\"^^xsd:int"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_ill_formed_xsd_integer() -> Result<(), String> {
    // "abc"^^xsd:integer has a non-numeric lexical form; ill-formed.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "abc", XSD_INTEGER,
    )]);
    r.reason();
    assert!(
        r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "expected rdfs-datatype diagnostic for non-numeric xsd:integer literal"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_well_formed_signed_xsd_integer() -> Result<(), String> {
    // Signed integers ("+7", "-42") are well-formed lexical forms for xsd:integer.
    let mut r = Reasoner::new();
    r.load_triples(vec![
        typed_literal_triple("urn:s", "urn:p", "-42", XSD_INTEGER),
        typed_literal_triple("urn:s", "urn:p", "+7", XSD_INTEGER),
    ]);
    r.reason();
    assert!(
        !r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "signed xsd:integer literals (-42, +7) should be well-formed"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_xsd_int_overflow() -> Result<(), String> {
    // xsd:int is 32-bit; a value outside i32 range is ill-formed.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s",
        "urn:p",
        "99999999999999999999",
        XSD_INT,
    )]);
    r.reason();
    assert!(
        r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "expected rdfs-datatype diagnostic for xsd:int literal outside i32 range"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_ill_formed_xml_literal() -> Result<(), String> {
    // An rdf:XMLLiteral whose lexical form does not close its single open tag
    // is ill-formed.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s",
        "urn:p",
        "<unclosed",
        RDF_XML_LITERAL,
    )]);
    r.reason();
    assert!(
        r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "expected rdfs-datatype diagnostic for ill-formed rdf:XMLLiteral"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_ill_formed_xml_literal_mismatched_tags() -> Result<(), String> {
    // Structural well-formedness: <a><b></a></b> has interleaved tags and is
    // not well-formed XML. The bracket-counting heuristic missed this; the
    // quick-xml parser catches it.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s",
        "urn:p",
        "<a><b></a></b>",
        RDF_XML_LITERAL,
    )]);
    r.reason();
    assert!(
        r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "expected rdfs-datatype diagnostic for mismatched-tag rdf:XMLLiteral"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_well_formed_xml_literal_no_error() -> Result<(), String> {
    // A correctly nested XMLLiteral must not raise a diagnostic.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s",
        "urn:p",
        "<a><b/></a>",
        RDF_XML_LITERAL,
    )]);
    r.reason();
    assert!(
        !r.errors().iter().any(|e| e.rule() == "rdfs-datatype"),
        "well-formed rdf:XMLLiteral should not raise a diagnostic"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_range_clash_string_for_integer() -> Result<(), String> {
    // Predicate range is xsd:integer; object is "abc"^^xsd:string. Range clash.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:p", RDFS_RANGE, XSD_INTEGER)]);
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "abc", XSD_STRING,
    )]);
    r.reason();
    assert!(
        r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype-range"),
        "expected rdfs-datatype-range diagnostic when object's datatype is not in range"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_range_clash_added_incrementally() -> Result<(), String> {
    // Retroactive range clash: a literal triple loaded first looks fine; then
    // a later batch declares rdfs:range on its predicate, retroactively
    // invalidating the literal. The post-fixpoint validator must catch this
    // even though the literal triple itself is not in the second batch's delta.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "abc", XSD_STRING,
    )]);
    r.reason();
    assert!(
        !r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype-range"),
        "no diagnostic expected before the range is declared"
    );
    r.load_triples_str(vec![("urn:p", RDFS_RANGE, XSD_INTEGER)]);
    r.reason();
    assert!(
        r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype-range"),
        "expected rdfs-datatype-range diagnostic after rdfs:range was added incrementally"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_range_compatible_integer() -> Result<(), String> {
    // Predicate range is xsd:integer; both xsd:integer and xsd:int objects
    // are inside the value space of xsd:integer (xsd:int ⊂ xsd:integer).
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:p", RDFS_RANGE, XSD_INTEGER)]);
    r.load_triples(vec![
        typed_literal_triple("urn:s", "urn:p", "42", XSD_INTEGER),
        typed_literal_triple("urn:s2", "urn:p", "7", XSD_INT),
    ]);
    r.reason();
    assert!(
        !r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype-range"),
        "xsd:integer and xsd:int literals should both satisfy range xsd:integer"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_range_clash_langstring_for_string() -> Result<(), String> {
    // W3C rdf-mt: rdfms-xmllang-test007a (plain string vs language-tagged).
    // Predicate range is xsd:string; object is "chat"@fr (rdf:langString) →
    // range clash, because a language-tagged literal is not in xsd:string's
    // value space.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("http://example.org/property", RDFS_RANGE, XSD_STRING)]);
    r.load_triples(vec![lang_literal_triple(
        "http://example.org/node",
        "http://example.org/property",
        "chat",
        "fr",
    )]);
    r.reason();
    assert!(
        r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype-range"),
        "expected rdfs-datatype-range diagnostic when xsd:string range receives rdf:langString"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_no_error_without_range_or_ill_formed() -> Result<(), String> {
    // Sanity: a well-formed literal whose predicate has no rdfs:range
    // and whose datatype is recognised produces no diagnostics.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "42", XSD_INTEGER,
    )]);
    r.reason();
    assert!(
        !r.errors()
            .iter()
            .any(|e| e.rule() == "rdfs-datatype" || e.rule() == "rdfs-datatype-range"),
        "a well-formed literal with no range constraint should not raise datatype diagnostics"
    );
    Ok(())
}

#[test]
fn test_rdfs_datatype_diagnostic_code() -> Result<(), String> {
    // Locks in the stable diagnostic code for the rdfs-datatype rule.
    let mut r = Reasoner::new();
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "abc", XSD_INTEGER,
    )]);
    r.reason();
    let has_code = r
        .errors()
        .iter()
        .any(|e| e.code() == "RDFS.DATATYPE" && e.rule() == "rdfs-datatype");
    assert!(has_code, "expected diagnostic with code RDFS.DATATYPE and rule rdfs-datatype");
    Ok(())
}

#[test]
fn test_rdfs_datatype_range_diagnostic_code() -> Result<(), String> {
    // Locks in the stable diagnostic code for the rdfs-datatype-range rule.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:p", RDFS_RANGE, XSD_INTEGER)]);
    r.load_triples(vec![typed_literal_triple(
        "urn:s", "urn:p", "abc", XSD_STRING,
    )]);
    r.reason();
    let has_code = r
        .errors()
        .iter()
        .any(|e| e.code() == "RDFS.DATATYPE_RANGE" && e.rule() == "rdfs-datatype-range");
    assert!(
        has_code,
        "expected diagnostic with code RDFS.DATATYPE_RANGE and rule rdfs-datatype-range"
    );
    Ok(())
}

//#[test]
//fn test_triple_update1() -> Result<(), String> {
//    let mut u = TripleUpdate::new();
//    let t1 = triple!("x1", "y1", "z1");
//    let t1rem = triple!("x1", "y1", "z1");
//    let t2 = triple!("x2", "y2", "z2");
//    u.add_triple(t1);
//    u.add_triple(t2);
//    u.remove_triple(t1rem);
//    assert_eq!(*u.updates.get(&triple!("x1", "y1", "z1")).unwrap(), 0);
//    assert_eq!(*u.updates.get(&triple!("x2", "y2", "z2")).unwrap(), 1);
//    Ok(())
//}
//
//#[test]
//fn test_triple_update2() -> Result<(), String> {
//    let mut u = TripleUpdate::new();
//    let t1 = triple!("x1", "y1", "z1");
//    let t2 = triple!("x2", "y2", "z2");
//    u.add_triple(t1);
//    u.add_triple(t2);
//    assert_eq!(*u.updates.get(&triple!("x1", "y1", "z1")).unwrap(), 1);
//    assert_eq!(*u.updates.get(&triple!("x2", "y2", "z2")).unwrap(), 1);
//    Ok(())
//}
//
//#[test]
//fn test_triple_update3() -> Result<(), String> {
//    let mut u = TripleUpdate::new();
//    let t1a = triple!("x1", "y1", "z1");
//    let t1b = triple!("x1", "y1", "z1");
//    let t1c = triple!("x1", "y1", "z1");
//    let t2 = triple!("x2", "y2", "z2");
//    u.add_triple(t1a);
//    u.add_triple(t1b);
//    u.add_triple(t2);
//    assert_eq!(*u.updates.get(&triple!("x1", "y1", "z1")).unwrap(), 2);
//    assert_eq!(*u.updates.get(&triple!("x2", "y2", "z2")).unwrap(), 1);
//    u.remove_triple(t1c);
//    assert_eq!(*u.updates.get(&triple!("x1", "y1", "z1")).unwrap(), 1);
//    Ok(())
//}
//
//#[test]
//fn test_manager_update() -> Result<(), String> {
//    let mut mgr = Manager::new_in_memory();
//
//    let mut u = TripleUpdate::new();
//    u.add_triple(triple!("x1", "y1", "z1"));
//
//    assert_eq!(mgr.size(), 0);
//    mgr.process_updates(u);
//    assert_eq!(mgr.size(), 6);
//
//    let mut u = TripleUpdate::new();
//    u.remove_triple(triple!("x1", "y1", "z1"));
//    mgr.process_updates(u);
//    println!("{}", mgr.dump_string());
//    assert_eq!(mgr.size(), 4);
//
//    let mut u = TripleUpdate::new();
//    u.add_triple(triple!("x3", "y3", "z3"));
//    u.add_triple(triple!("x1", "y1", "z1"));
//    mgr.process_updates(u);
//    assert_eq!(mgr.size(), 8);
//
//    Ok(())
//}

// ==================== Incremental materialization tests ====================

/// Helper: runs both full and incremental materialization on the same data
/// and asserts they produce identical results.
fn assert_incremental_equivalent(
    batch1: Vec<(&'static str, &'static str, &'static str)>,
    batch2: Vec<(&'static str, &'static str, &'static str)>,
) {
    // Full materialization: load all triples at once
    let mut full = Reasoner::new();
    let mut all = batch1.clone();
    all.extend(batch2.clone());
    full.load_triples_str(all);
    full.reason();
    let mut full_result = full.get_triples_string();
    full_result.sort();

    // Incremental materialization: load batch1 → reason → load batch2 → reason
    let mut incr = Reasoner::new();
    incr.load_triples_str(batch1);
    incr.reason();
    incr.load_triples_str(batch2);
    incr.reason();
    let mut incr_result = incr.get_triples_string();
    incr_result.sort();

    assert_eq!(
        full_result, incr_result,
        "Incremental materialization produced different results than full materialization"
    );
}

#[test]
fn test_incremental_cax_sco() {
    // Ontology: Person subClassOf Agent
    // Batch 1: ontology
    // Batch 2: alice rdf:type Person → should infer alice rdf:type Agent
    assert_incremental_equivalent(
        vec![("urn:Person", RDFS_SUBCLASSOF, "urn:Agent")],
        vec![("urn:alice", RDF_TYPE, "urn:Person")],
    );
}

#[test]
fn test_incremental_eq_sym() {
    assert_incremental_equivalent(
        vec![("urn:x", OWL_SAMEAS, "urn:y")],
        vec![("urn:y", OWL_SAMEAS, "urn:z")],
    );
}

#[test]
fn test_incremental_eq_trans() {
    assert_incremental_equivalent(
        vec![("urn:x", OWL_SAMEAS, "urn:y")],
        vec![("urn:y", OWL_SAMEAS, "urn:z")],
    );
}

#[test]
fn test_incremental_eq_rep_s() {
    // Adding sameAs should propagate to existing triples
    assert_incremental_equivalent(
        vec![("urn:alice", "urn:knows", "urn:bob")],
        vec![("urn:alice", OWL_SAMEAS, "urn:alice2")],
    );
}

#[test]
fn test_incremental_prp_spo1() {
    assert_incremental_equivalent(
        vec![("urn:hasFather", RDFS_SUBPROP, "urn:hasParent")],
        vec![("urn:bob", "urn:hasFather", "urn:john")],
    );
}

#[test]
fn test_incremental_prp_dom() {
    assert_incremental_equivalent(
        vec![("urn:knows", RDFS_DOMAIN, "urn:Person")],
        vec![("urn:alice", "urn:knows", "urn:bob")],
    );
}

#[test]
fn test_incremental_prp_rng() {
    assert_incremental_equivalent(
        vec![("urn:knows", RDFS_RANGE, "urn:Person")],
        vec![("urn:alice", "urn:knows", "urn:bob")],
    );
}

#[test]
fn test_incremental_prp_inv() {
    assert_incremental_equivalent(
        vec![("urn:hasChild", OWL_INVERSEOF, "urn:hasParent")],
        vec![("urn:bob", "urn:hasChild", "urn:charlie")],
    );
}

#[test]
fn test_incremental_prp_symp() {
    assert_incremental_equivalent(
        vec![
            ("urn:friendOf", RDF_TYPE, OWL_SYMMETRICPROP),
        ],
        vec![("urn:alice", "urn:friendOf", "urn:bob")],
    );
}

#[test]
fn test_incremental_prp_trp() {
    assert_incremental_equivalent(
        vec![
            ("urn:ancestor", RDF_TYPE, OWL_TRANSPROP),
            ("urn:a", "urn:ancestor", "urn:b"),
        ],
        vec![("urn:b", "urn:ancestor", "urn:c")],
    );
}

#[test]
fn test_incremental_prp_fp() {
    assert_incremental_equivalent(
        vec![
            ("urn:hasMother", RDF_TYPE, OWL_FUNCPROP),
            ("urn:bob", "urn:hasMother", "urn:mary"),
        ],
        vec![("urn:bob", "urn:hasMother", "urn:maria")],
    );
}

#[test]
fn test_incremental_prp_eqp() {
    assert_incremental_equivalent(
        vec![("urn:cost", OWL_EQUIVPROP, "urn:price")],
        vec![("urn:item1", "urn:cost", "urn:10")],
    );
}

#[test]
fn test_incremental_cax_eqc() {
    assert_incremental_equivalent(
        vec![("urn:Human", OWL_EQUIVALENTCLASS, "urn:Person")],
        vec![("urn:alice", RDF_TYPE, "urn:Human")],
    );
}

#[test]
fn test_incremental_subclass_chain() {
    // Test cascading: A subClassOf B, B subClassOf C, then add instance of A
    assert_incremental_equivalent(
        vec![
            ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
            ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
        ],
        vec![("urn:x", RDF_TYPE, "urn:A")],
    );
}

#[test]
fn test_incremental_rdfs_container_membership() {
    // rdf:_N predicates introduced in an incremental batch must still trigger
    // the container-membership axiom injection so that:
    //   rdf:_N rdf:type rdfs:ContainerMembershipProperty
    //   rdf:_N rdfs:subPropertyOf rdfs:member
    //   <s> rdfs:member <o>   (via prp-spo1)
    // all appear in the closure — i.e. incremental must match full materialization.
    assert_incremental_equivalent(
        vec![("urn:bootstrap", RDF_TYPE, "urn:Thing")],
        vec![(
            "urn:a",
            "http://www.w3.org/1999/02/22-rdf-syntax-ns#_1",
            "urn:b",
        )],
    );
}

#[test]
fn test_incremental_cls_union() {
    // x is union of A and B. Add instance of A → should infer instance of x.
    assert_incremental_equivalent(
        vec![
            ("urn:x", OWL_UNION, "urn:list1"),
            ("urn:list1", RDF_FIRST, "urn:A"),
            ("urn:list1", RDF_REST, "urn:list2"),
            ("urn:list2", RDF_FIRST, "urn:B"),
            ("urn:list2", RDF_REST, RDF_NIL),
        ],
        vec![("urn:alice", RDF_TYPE, "urn:A")],
    );
}

#[test]
fn test_incremental_cls_intersection() {
    // x is intersection of A and B. Add an instance of both A and B.
    assert_incremental_equivalent(
        vec![
            ("urn:x", OWL_INTERSECTION, "urn:list1"),
            ("urn:list1", RDF_FIRST, "urn:A"),
            ("urn:list1", RDF_REST, "urn:list2"),
            ("urn:list2", RDF_FIRST, "urn:B"),
            ("urn:list2", RDF_REST, RDF_NIL),
            ("urn:alice", RDF_TYPE, "urn:A"),
        ],
        vec![("urn:alice", RDF_TYPE, "urn:B")],
    );
}

#[test]
fn test_incremental_cls_hasvalue() {
    assert_incremental_equivalent(
        vec![
            ("urn:r", OWL_HASVALUE, "urn:v"),
            ("urn:r", OWL_ONPROPERTY, "urn:p"),
        ],
        vec![("urn:alice", RDF_TYPE, "urn:r")],
    );
}

#[test]
fn test_incremental_reason_full_matches_incremental() {
    // Verify that reason_full() produces the same result as incremental
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:Person", RDFS_SUBCLASSOF, "urn:Agent")]);
    r.reason();
    r.load_triples_str(vec![("urn:alice", RDF_TYPE, "urn:Person")]);
    r.reason();
    let mut incr_result = r.get_triples_string();
    incr_result.sort();

    r.reason_full();
    let mut full_result = r.get_triples_string();
    full_result.sort();

    assert_eq!(incr_result, full_result);
}

#[test]
fn test_incremental_noop_when_no_delta() {
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:a", RDF_TYPE, "urn:B")]);
    r.reason();
    let result1 = r.get_triples_string();
    // Calling reason() again without adding triples should be a no-op
    r.reason();
    let result2 = r.get_triples_string();
    assert_eq!(result1, result2);
}

#[test]
fn test_incremental_multiple_batches() {
    // Add triples in 3 separate incremental batches
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
    ]);
    r.reason();

    r.load_triples_str(vec![("urn:x", RDF_TYPE, "urn:A")]);
    r.reason();

    r.load_triples_str(vec![("urn:y", RDF_TYPE, "urn:B")]);
    r.reason();

    let mut incr_result = r.get_triples_string();
    incr_result.sort();

    // Compare with full materialization
    let mut full = Reasoner::new();
    full.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:B", RDFS_SUBCLASSOF, "urn:C"),
        ("urn:x", RDF_TYPE, "urn:A"),
        ("urn:y", RDF_TYPE, "urn:B"),
    ]);
    full.reason();
    let mut full_result = full.get_triples_string();
    full_result.sort();

    assert_eq!(incr_result, full_result);
}

// ==================== Retraction / clear() behavior tests ====================

#[test]
fn test_clear_and_rematerialize_without_retracted_triple() {
    // Simulate retraction via clear() + reload without the removed triple.
    // Start with: A subClassOf B, x rdf:type A → infers x rdf:type B.
    // Then "retract" the subClassOf and re-materialize → x rdf:type B should disappear.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();
    let res = r.get_triples_string();
    assert!(
        res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "Before retraction: x should be inferred as type B"
    );

    // "Retract" the subClassOf by rebuilding from scratch without it
    let mut r2 = Reasoner::new();
    r2.load_triples_str(vec![("urn:x", RDF_TYPE, "urn:A")]);
    r2.reason();
    let res2 = r2.get_triples_string();
    assert!(
        !res2.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "After retraction: x should NOT be inferred as type B"
    );
}

#[test]
fn test_clear_resets_to_base_triples() {
    // clear() resets to base triples (all triples ever loaded), not to empty.
    // After clear(), reason() performs a full re-materialization from base.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();

    // clear() discards inferred triples but retains all loaded (base) triples
    r.clear();
    r.reason();

    let mut res = r.get_triples_string();
    res.sort();

    // Should match a fresh reasoner with the SAME base input
    let mut fresh = Reasoner::new();
    fresh.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    fresh.reason();
    let mut fresh_res = fresh.get_triples_string();
    fresh_res.sort();

    assert_eq!(res, fresh_res, "clear() + reason() should re-derive the same closure from base");
}

#[test]
fn test_clear_then_incremental_works() {
    // After clear() + reason(), the reasoner should support incremental again.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    r.reason();

    r.clear();
    r.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    r.reason(); // Full re-materialization

    // Now add incrementally
    r.load_triples_str(vec![("urn:x", RDF_TYPE, "urn:A")]);
    r.reason(); // Incremental

    let mut res = r.get_triples_string();
    res.sort();

    // Compare with fresh full materialization
    let mut fresh = Reasoner::new();
    fresh.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    fresh.reason();
    let mut fresh_res = fresh.get_triples_string();
    fresh_res.sort();

    assert_eq!(res, fresh_res, "clear() → reason() → incremental should work correctly");
}

#[test]
fn test_reason_full_simulates_retraction() {
    // reason_full() re-derives from base triples only. If we modify base
    // (via clear + reload), reason_full() should reflect the change.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();

    // Incrementally add more data
    r.load_triples_str(vec![("urn:y", RDF_TYPE, "urn:A")]);
    r.reason();

    // Now reason_full() should produce the same result (base includes all loaded triples)
    let mut before = r.get_triples_string();
    before.sort();

    r.reason_full();
    let mut after = r.get_triples_string();
    after.sort();

    assert_eq!(before, after, "reason_full() should match incremental result");
}

#[test]
fn test_incremental_does_not_support_retraction() {
    // Document that incremental materialization does NOT support retraction.
    // Once a triple is loaded, it becomes part of the base and persists across
    // clear() calls. The only way to truly retract is to create a new Reasoner.
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    r.reason();

    // Add an instance
    r.load_triples_str(vec![("urn:x", RDF_TYPE, "urn:A")]);
    r.reason();

    let res = r.get_triples_string();
    assert!(
        res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "x should be inferred as type B"
    );

    // There is no way to remove a triple incrementally.
    // Calling reason() again without adding anything is a no-op.
    r.reason();
    let res2 = r.get_triples_string();
    assert!(
        res2.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "Inferred triples persist — no retraction support in incremental mode"
    );

    // clear() resets inferred state but base triples persist, so the
    // inference is re-derived on the next reason() call.
    r.clear();
    r.reason();
    let res3 = r.get_triples_string();
    assert!(
        res3.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "clear() retains base triples — inference is re-derived"
    );

    // The ONLY way to truly retract is to create a new Reasoner without the triple.
    let mut r2 = Reasoner::new();
    r2.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    // Deliberately NOT loading (x, rdf:type, A)
    r2.reason();

    let res4 = r2.get_triples_string();
    assert!(
        !res4.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "New reasoner without x: the inference should be gone"
    );
}

// ==================== set_base_triples() tests ====================

/// Helper to build oxrdf triples from string URIs for use with set_base_triples()
fn make_test_triples(trips: Vec<(&str, &str, &str)>) -> Vec<oxrdf::Triple> {
    use crate::common::make_triple;
    trips
        .into_iter()
        .map(|(s, p, o)| {
            make_triple(
                oxrdf::Term::NamedNode(oxrdf::NamedNode::new(s).unwrap()),
                oxrdf::Term::NamedNode(oxrdf::NamedNode::new(p).unwrap()),
                oxrdf::Term::NamedNode(oxrdf::NamedNode::new(o).unwrap()),
            )
            .unwrap()
        })
        .collect()
}

#[test]
fn test_set_base_triples_additions_only() {
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    r.reason();

    // set_base_triples with a superset (adds x rdf:type A)
    let needs_full = r.set_base_triples(make_test_triples(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]));
    assert!(!needs_full, "Additions only should not require full re-materialization");

    r.reason();
    let res = r.get_triples_string();
    assert!(
        res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "Incremental: x should be inferred as type B"
    );
}

#[test]
fn test_set_base_triples_with_removals() {
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();

    let res = r.get_triples_string();
    assert!(res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())));

    // Remove (x, rdf:type, A) by setting base to just the subClassOf triple
    let needs_full = r.set_base_triples(make_test_triples(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
    ]));
    assert!(needs_full, "Removals should require full re-materialization");

    r.reason();
    let res = r.get_triples_string();
    assert!(
        !res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "After removing x from base, inference should be gone"
    );
}

#[test]
fn test_set_base_triples_mixed() {
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();

    // Replace: remove x, add y
    let needs_full = r.set_base_triples(make_test_triples(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:y", RDF_TYPE, "urn:A"),
    ]));
    assert!(needs_full, "Mixed add+remove should require full re-materialization");

    r.reason();
    let res = r.get_triples_string();
    assert!(
        !res.contains(&("<urn:x>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "x inference should be gone"
    );
    assert!(
        res.contains(&("<urn:y>".to_string(), wrap!(RDF_TYPE), "<urn:B>".to_string())),
        "y inference should be present"
    );
}

#[test]
fn test_set_base_triples_no_change() {
    let mut r = Reasoner::new();
    r.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    r.reason();
    let res1 = r.get_triples_string();

    // Set identical base
    let needs_full = r.set_base_triples(make_test_triples(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]));
    assert!(!needs_full, "No change should be a no-op");

    r.reason(); // Should be no-op since no delta
    let res2 = r.get_triples_string();
    assert_eq!(res1, res2, "No change in base should produce identical output");
}

#[test]
fn test_set_base_triples_equivalence() {
    // Additions-only via set_base_triples should match fresh full materialization
    let mut r = Reasoner::new();
    r.load_triples_str(vec![("urn:A", RDFS_SUBCLASSOF, "urn:B")]);
    r.reason();

    r.set_base_triples(make_test_triples(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]));
    r.reason();
    let mut incr = r.get_triples_string();
    incr.sort();

    let mut full = Reasoner::new();
    full.load_triples_str(vec![
        ("urn:A", RDFS_SUBCLASSOF, "urn:B"),
        ("urn:x", RDF_TYPE, "urn:A"),
    ]);
    full.reason();
    let mut full_res = full.get_triples_string();
    full_res.sort();

    assert_eq!(incr, full_res, "Incremental set_base_triples should match full materialization");
}
