reasonable 0.4.0-a2

//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_LITERAL: &str = "http://www.w3.org/2000/01/rdf-schema#Literal";
const RDFS_RESOURCE: &str = "http://www.w3.org/2000/01/rdf-schema#Resource";
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 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_RESTRICTION: &str = "http://www.w3.org/2002/07/owl#Restriction";
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)
    };
}

macro_rules! triple {
    ($s:expr, $p:expr, $o:expr) => {
        make_triple(uri!("urn:{}", $s), uri!("urn:{}", $p), uri!("urn:{}", $o)).unwrap()
    };
}

#[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(())
}

//#[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_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");
}