From 12f99d4142af6b22b80d1db6246c0e488b5a13bc Mon Sep 17 00:00:00 2001 From: alkidbaci Date: Thu, 9 Apr 2026 16:20:12 +0200 Subject: [PATCH 1/2] added support for data cardinality restrictions --- owlapy/owl_reasoner.py | 179 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 178 insertions(+), 1 deletion(-) diff --git a/owlapy/owl_reasoner.py b/owlapy/owl_reasoner.py index 1db4101b..1884db54 100644 --- a/owlapy/owl_reasoner.py +++ b/owlapy/owl_reasoner.py @@ -18,7 +18,7 @@ OWLObjectIntersectionOf, OWLObjectComplementOf, OWLObjectAllValuesFrom, OWLObjectOneOf, OWLObjectHasValue, \ OWLObjectMinCardinality, OWLObjectMaxCardinality, OWLObjectExactCardinality, OWLObjectCardinalityRestriction, \ OWLDataSomeValuesFrom, OWLDataOneOf, OWLDatatypeRestriction, OWLFacetRestriction, OWLDataHasValue, \ - OWLDataAllValuesFrom, OWLNothing, OWLThing + OWLDataAllValuesFrom, OWLNothing, OWLThing, OWLDataMinCardinality, OWLDataMaxCardinality, OWLDataExactCardinality from owlapy.class_expression import OWLClass from owlapy.iri import IRI from owlapy.owl_axiom import OWLAxiom, OWLSubClassOfAxiom @@ -989,6 +989,183 @@ def _lazy_cache_class(self, c: OWLClass) -> None: temp = self.get_instances_from_owl_class(c) self._cls_to_ind[c] = frozenset(temp) + @_find_instances.register + def _(self, ce: OWLDataMinCardinality): + return self._get_instances_data_card_restriction(ce) + + @_find_instances.register + def _(self, ce: OWLDataMaxCardinality): + all_ = frozenset(self._ontology.individuals_in_signature()) + min_ind = self._get_instances_data_card_restriction( + OWLDataMinCardinality(cardinality=ce.get_cardinality() + 1, + property=ce.get_property(), + filler=ce.get_filler())) + return all_ ^ min_ind + + @_find_instances.register + def _(self, ce: OWLDataExactCardinality): + return self._get_instances_data_card_restriction(ce) + + def _get_instances_data_card_restriction(self, ce) -> FrozenSet[OWLNamedIndividual]: + """Get instances for OWLDataMinCardinality or OWLDataExactCardinality restrictions.""" + pe = ce.get_property() + filler = ce.get_filler() + assert isinstance(pe, OWLDataProperty) + + if isinstance(ce, OWLDataMinCardinality): + min_count = ce.get_cardinality() + max_count = None + elif isinstance(ce, OWLDataExactCardinality): + min_count = max_count = ce.get_cardinality() + else: + raise NotImplementedError + + assert min_count >= 0 + assert max_count is None or max_count >= 0 + + if self._ontology.is_modified and (self.class_cache or self._property_cache): + self.reset_and_disable_cache() + property_cache = self._property_cache + + if property_cache: + self._lazy_cache_data_prop(pe) + dps = self._data_prop[pe] + else: + subs = self._some_values_subject_index(pe) + + ind = set() + + if isinstance(filler, OWLDatatype): + if property_cache: + for s, literals in dps.items(): + count = sum(1 for lit in literals if lit.get_datatype() == filler) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + count = sum(1 for lit in self.data_property_values(s, pe) if lit.get_datatype() == filler) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + elif isinstance(filler, OWLDataOneOf): + values = set(filler.values()) + if property_cache: + for s, literals in dps.items(): + count = len(literals & values) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + count = sum(1 for lit in self.data_property_values(s, pe) if lit in values) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + elif isinstance(filler, OWLDatatypeRestriction): + def res_to_callable(res: OWLFacetRestriction): + op = res.get_facet().operator + v = res.get_facet_value() + + def inner(lv: OWLLiteral): + return op(lv, v) + + return inner + + apply = FunctionType.__call__ + facet_restrictions = tuple(map(res_to_callable, filler.get_facet_restrictions())) + + def include(lv: OWLLiteral): + return lv.get_datatype() == filler.get_datatype() and \ + all(map(apply, facet_restrictions, repeat(lv))) + + if property_cache: + for s, literals in dps.items(): + count = sum(1 for lit in literals if include(lit)) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + count = sum(1 for lit in self.data_property_values(s, pe) if include(lit)) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + elif isinstance(filler, OWLDataComplementOf): + # Count values NOT matching the inner data range + inner_filler = filler.get_data_range() + # some_inner = OWLDataSomeValuesFrom(property=pe, filler=inner_filler) + # We need to count per-individual, so we iterate + if property_cache: + for s, literals in dps.items(): + # Count literals that match the complement (i.e., do NOT match the inner filler) + match_inner = self._count_data_filler_matches(literals, inner_filler) + count = len(literals) - match_inner + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + all_lits = set(self.data_property_values(s, pe)) + match_inner = self._count_data_filler_matches(all_lits, inner_filler) + count = len(all_lits) - match_inner + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + elif isinstance(filler, OWLDataUnionOf): + if property_cache: + for s, literals in dps.items(): + count = sum(1 for lit in literals + if any(self._literal_matches_data_range(lit, op) + for op in filler.operands())) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + count = sum(1 for lit in self.data_property_values(s, pe) + if any(self._literal_matches_data_range(lit, op) + for op in filler.operands())) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + elif isinstance(filler, OWLDataIntersectionOf): + if property_cache: + for s, literals in dps.items(): + count = sum(1 for lit in literals + if all(self._literal_matches_data_range(lit, op) + for op in filler.operands())) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + for s in subs: + count = sum(1 for lit in self.data_property_values(s, pe) + if all(self._literal_matches_data_range(lit, op) + for op in filler.operands())) + if count >= min_count and (max_count is None or count <= max_count): + ind.add(s) + else: + raise ValueError + + return frozenset(ind) + + def _literal_matches_data_range(self, lit: OWLLiteral, dr) -> bool: + """Check if a single literal matches a data range.""" + if isinstance(dr, OWLDatatype): + return lit.get_datatype() == dr + elif isinstance(dr, OWLDataOneOf): + return lit in set(dr.values()) + elif isinstance(dr, OWLDatatypeRestriction): + if lit.get_datatype() != dr.get_datatype(): + return False + for res in dr.get_facet_restrictions(): + op = res.get_facet().operator + if not op(lit, res.get_facet_value()): + return False + return True + elif isinstance(dr, OWLDataComplementOf): + return not self._literal_matches_data_range(lit, dr.get_data_range()) + elif isinstance(dr, OWLDataUnionOf): + return any(self._literal_matches_data_range(lit, op) for op in dr.operands()) + elif isinstance(dr, OWLDataIntersectionOf): + return all(self._literal_matches_data_range(lit, op) for op in dr.operands()) + else: + raise ValueError(f"Unsupported data range type: {type(dr)}") + + def _count_data_filler_matches(self, literals: Set[OWLLiteral], dr) -> int: + """Count how many literals in the set match the given data range.""" + return sum(1 for lit in literals if self._literal_matches_data_range(lit, dr)) + def get_instances_from_owl_class(self, c: OWLClass): if c.is_owl_thing(): yield from self._ontology.individuals_in_signature() From 95d2f8021897c8517d5df813306c33b2956bd2dc Mon Sep 17 00:00:00 2001 From: alkidbaci Date: Thu, 9 Apr 2026 16:22:41 +0200 Subject: [PATCH 2/2] added test for data cardinality restrictions --- tests/test_data_cardinality_restrictions.py | 480 ++++++++++++++++++++ 1 file changed, 480 insertions(+) create mode 100644 tests/test_data_cardinality_restrictions.py diff --git a/tests/test_data_cardinality_restrictions.py b/tests/test_data_cardinality_restrictions.py new file mode 100644 index 00000000..35b98989 --- /dev/null +++ b/tests/test_data_cardinality_restrictions.py @@ -0,0 +1,480 @@ +""" +Unit tests for OWLDataMinCardinality, OWLDataMaxCardinality, and OWLDataExactCardinality +_find_instances specializations in StructuralReasoner, using the Mutagenesis dataset. + +Key dataset facts (Mutagenesis): + - Total individuals: 14145 + - Individuals with 'charge' (xsd:double, exactly 1 per individual): 5894 + - Individuals with 'lumo' (xsd:double, exactly 1 per individual): 230 + - Individuals with 'act' (xsd:double, exactly 1 per individual): 230 + - No individual has more than 1 value for any single data property +""" +import unittest + +from owlapy.class_expression import ( + OWLDataMinCardinality, + OWLDataMaxCardinality, + OWLDataExactCardinality, + OWLDataSomeValuesFrom, + OWLClass, +) +from owlapy.iri import IRI +from owlapy.owl_datatype import OWLDatatype +from owlapy.owl_individual import OWLNamedIndividual +from owlapy.owl_ontology import Ontology +from owlapy.owl_property import OWLDataProperty +from owlapy.owl_reasoner import StructuralReasoner +from owlapy.providers import ( + owl_datatype_min_inclusive_restriction, + owl_datatype_min_max_inclusive_restriction, + owl_datatype_max_inclusive_restriction, +) +from owlapy.vocab import XSDVocabulary + + +NS = "http://dl-learner.org/mutagenesis#" +ONTOLOGY_PATH = "KGs/Mutagenesis/mutagenesis.owl" + +# Known cardinalities derived from the dataset +TOTAL_INDIVIDUALS = 14145 +INDIVIDUALS_WITH_CHARGE = 5894 # atoms that have a 'charge' double value +INDIVIDUALS_WITH_LUMO = 230 # compounds that have a 'lumo' double value +INDIVIDUALS_WITH_ACT = 230 # compounds that have an 'act' double value +INDIVIDUALS_WITH_POSITIVE_CHARGE = 2925 # charge >= 0.0 + + +class TestDataCardinalityRestrictionsWithDatatype(unittest.TestCase): + """ + Tests for OWLDataMinCardinality, OWLDataMaxCardinality, OWLDataExactCardinality + using xsd:double as the filler (bare datatype). + """ + + @classmethod + def setUpClass(cls): + cls.onto = Ontology(ONTOLOGY_PATH) + cls.reasoner = StructuralReasoner(cls.onto) + cls.all_inds = frozenset(cls.onto.individuals_in_signature()) + + cls.charge_dp = OWLDataProperty(IRI(NS, "charge")) + cls.lumo_dp = OWLDataProperty(IRI(NS, "lumo")) + cls.act_dp = OWLDataProperty(IRI(NS, "act")) + cls.double_type = OWLDatatype(XSDVocabulary.DOUBLE) + + # ------------------------------------------------------------------ + # OWLDataMinCardinality – xsd:double filler + # ------------------------------------------------------------------ + + def test_min_cardinality_1_charge_double_returns_all_atoms_with_charge(self): + """Min(1, charge, xsd:double) should match all atoms having a charge value.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_CHARGE) + + def test_min_cardinality_2_charge_double_returns_empty(self): + """Min(2, charge, xsd:double) should be empty: no individual has 2+ charge values.""" + ce = OWLDataMinCardinality(cardinality=2, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), 0) + + def test_min_cardinality_0_charge_double_returns_all_with_charge(self): + """Min(0, charge, xsd:double) should match everything that has >=0 matching values. + Because the cache only iterates individuals that have the property, this equals + the set of individuals possessing a charge value.""" + ce = OWLDataMinCardinality(cardinality=0, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + # Every individual in dps satisfies count >= 0 + self.assertEqual(len(result), INDIVIDUALS_WITH_CHARGE) + + def test_min_cardinality_1_lumo_double(self): + """Min(1, lumo, xsd:double) should match all compounds with a lumo value.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_LUMO) + + def test_min_cardinality_1_act_double(self): + """Min(1, act, xsd:double) should match all compounds with an act value.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.act_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_ACT) + + # ------------------------------------------------------------------ + # OWLDataMaxCardinality – xsd:double filler + # ------------------------------------------------------------------ + + def test_max_cardinality_0_charge_double_is_complement_of_min1(self): + """Max(0, charge, xsd:double) == all_individuals - Min(1, charge, xsd:double).""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.double_type) + + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + + self.assertEqual(max0_result, self.all_inds - min1_result) + + def test_max_cardinality_0_charge_double_count(self): + """Max(0, charge, xsd:double) should return individuals without a charge value.""" + ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + expected_count = TOTAL_INDIVIDUALS - INDIVIDUALS_WITH_CHARGE + self.assertEqual(len(result), expected_count) + + def test_max_cardinality_1_charge_double_returns_all_individuals(self): + """Max(1, charge, xsd:double) should return all individuals because none has 2+ values.""" + ce = OWLDataMaxCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), TOTAL_INDIVIDUALS) + + def test_max_cardinality_0_lumo_double_count(self): + """Max(0, lumo, xsd:double) should return individuals without a lumo value.""" + ce = OWLDataMaxCardinality(cardinality=0, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + expected_count = TOTAL_INDIVIDUALS - INDIVIDUALS_WITH_LUMO + self.assertEqual(len(result), expected_count) + + # ------------------------------------------------------------------ + # OWLDataExactCardinality – xsd:double filler + # ------------------------------------------------------------------ + + def test_exact_cardinality_1_charge_double_equals_min1(self): + """Exact(1, charge, xsd:double) == Min(1, charge, xsd:double) when every atom has exactly 1 charge.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + exact1_ce = OWLDataExactCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + + min1_result = set(self.reasoner.instances(min1_ce)) + exact1_result = set(self.reasoner.instances(exact1_ce)) + + self.assertEqual(exact1_result, min1_result) + + def test_exact_cardinality_1_charge_double_count(self): + """Exact(1, charge, xsd:double) should return exactly 5894 atoms.""" + ce = OWLDataExactCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_CHARGE) + + def test_exact_cardinality_2_charge_double_is_empty(self): + """Exact(2, charge, xsd:double) should be empty because no individual has 2 charge values.""" + ce = OWLDataExactCardinality(cardinality=2, property=self.charge_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), 0) + + def test_exact_cardinality_1_lumo_double_count(self): + """Exact(1, lumo, xsd:double) should return the 230 compounds with exactly 1 lumo value.""" + ce = OWLDataExactCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_LUMO) + + # ------------------------------------------------------------------ + # Logical consistency checks + # ------------------------------------------------------------------ + + def test_min1_and_max0_are_disjoint(self): + """Min(1, charge, double) and Max(0, charge, double) must be disjoint.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.double_type) + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + self.assertEqual(min1_result & max0_result, set()) + + def test_min1_and_max0_cover_all_individuals(self): + """Min(1, charge, double) ∪ Max(0, charge, double) == all individuals.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.double_type) + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + self.assertEqual(min1_result | max0_result, self.all_inds) + + def test_min1_and_max0_lumo_cover_all_individuals(self): + """Min(1, lumo, double) ∪ Max(0, lumo, double) == all individuals.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.lumo_dp, + filler=self.double_type) + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + self.assertEqual(min1_result | max0_result, self.all_inds) + + def test_min1_subset_of_max1_for_charge(self): + """Min(1, charge, double) ⊆ Max(1, charge, double) (both include individuals with 1 value).""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + max1_ce = OWLDataMaxCardinality(cardinality=1, property=self.charge_dp, + filler=self.double_type) + min1_result = set(self.reasoner.instances(min1_ce)) + max1_result = set(self.reasoner.instances(max1_ce)) + self.assertTrue(min1_result.issubset(max1_result)) + + +class TestDataCardinalityRestrictionsWithDatatypeRestriction(unittest.TestCase): + """ + Tests using OWLDatatypeRestriction as filler (e.g., charge >= 0.0). + """ + + @classmethod + def setUpClass(cls): + cls.onto = Ontology(ONTOLOGY_PATH) + cls.reasoner = StructuralReasoner(cls.onto) + cls.all_inds = frozenset(cls.onto.individuals_in_signature()) + + cls.charge_dp = OWLDataProperty(IRI(NS, "charge")) + cls.lumo_dp = OWLDataProperty(IRI(NS, "lumo")) + + # Filler: charge >= 0.0 (positive or neutral charges) + cls.positive_charge_filler = owl_datatype_min_inclusive_restriction(0.0) + # Filler: lumo >= -1.5 + cls.lumo_gte_minus1_5 = owl_datatype_min_inclusive_restriction(-1.5) + + # ------------------------------------------------------------------ + # OWLDataMinCardinality – DatatypeRestriction filler + # ------------------------------------------------------------------ + + def test_min_cardinality_1_positive_charge(self): + """Min(1, charge, charge>=0) should match atoms with at least 1 non-negative charge.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_POSITIVE_CHARGE) + + def test_min_cardinality_2_positive_charge_is_empty(self): + """Min(2, charge, charge>=0) should be empty because each atom has at most 1 charge value.""" + ce = OWLDataMinCardinality(cardinality=2, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), 0) + + def test_min_cardinality_1_lumo_gte_minus1_5(self): + """Min(1, lumo, lumo>=-1.5) should match compounds whose lumo value is >= -1.5.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.lumo_gte_minus1_5) + result = set(self.reasoner.instances(ce)) + # Verify: same as OWLDataSomeValuesFrom(lumo, lumo>=-1.5) + svf = OWLDataSomeValuesFrom(property=self.lumo_dp, filler=self.lumo_gte_minus1_5) + svf_result = set(self.reasoner.instances(svf)) + self.assertEqual(result, svf_result) + self.assertEqual(len(result), 99) # 99 compounds have lumo >= -1.5 + + # ------------------------------------------------------------------ + # OWLDataMaxCardinality – DatatypeRestriction filler + # ------------------------------------------------------------------ + + def test_max_cardinality_0_positive_charge_count(self): + """Max(0, charge, charge>=0) should return individuals that have no non-negative charge value.""" + ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + expected = TOTAL_INDIVIDUALS - INDIVIDUALS_WITH_POSITIVE_CHARGE + self.assertEqual(len(result), expected) + + def test_max_cardinality_0_positive_charge_is_complement_of_min1(self): + """Max(0, charge, >=0) == all_individuals - Min(1, charge, >=0).""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.positive_charge_filler) + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + self.assertEqual(max0_result, self.all_inds - min1_result) + + def test_max_cardinality_1_positive_charge_returns_all(self): + """Max(1, charge, charge>=0) == all individuals because no atom has 2+ charge values.""" + ce = OWLDataMaxCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), TOTAL_INDIVIDUALS) + + # ------------------------------------------------------------------ + # OWLDataExactCardinality – DatatypeRestriction filler + # ------------------------------------------------------------------ + + def test_exact_cardinality_1_positive_charge(self): + """Exact(1, charge, charge>=0) should match atoms with exactly 1 non-negative charge.""" + ce = OWLDataExactCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_POSITIVE_CHARGE) + + def test_exact_cardinality_1_positive_charge_equals_min1(self): + """Exact(1, charge, >=0) == Min(1, charge, >=0) since each atom has at most 1 charge.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + exact1_ce = OWLDataExactCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + self.assertEqual(set(self.reasoner.instances(min1_ce)), + set(self.reasoner.instances(exact1_ce))) + + def test_exact_cardinality_2_positive_charge_is_empty(self): + """Exact(2, charge, charge>=0) should be empty.""" + ce = OWLDataExactCardinality(cardinality=2, property=self.charge_dp, + filler=self.positive_charge_filler) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), 0) + + # ------------------------------------------------------------------ + # Logical consistency checks + # ------------------------------------------------------------------ + + def test_min1_and_max0_positive_charge_cover_all(self): + """Min(1, charge, >=0) ∪ Max(0, charge, >=0) == all individuals.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.positive_charge_filler) + self.assertEqual(set(self.reasoner.instances(min1_ce)) | + set(self.reasoner.instances(max0_ce)), + self.all_inds) + + def test_min1_and_max0_positive_charge_are_disjoint(self): + """Min(1, charge, >=0) ∩ Max(0, charge, >=0) == ∅.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.positive_charge_filler) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.positive_charge_filler) + self.assertEqual(set(self.reasoner.instances(min1_ce)) & + set(self.reasoner.instances(max0_ce)), + set()) + + +class TestDataCardinalityRestrictionsWithRangeRestriction(unittest.TestCase): + """ + Tests using a bounded range (min_max inclusive) as the filler. + """ + + @classmethod + def setUpClass(cls): + cls.onto = Ontology(ONTOLOGY_PATH) + cls.reasoner = StructuralReasoner(cls.onto) + cls.all_inds = frozenset(cls.onto.individuals_in_signature()) + + cls.charge_dp = OWLDataProperty(IRI(NS, "charge")) + cls.lumo_dp = OWLDataProperty(IRI(NS, "lumo")) + + # Filler: -0.1 <= charge <= 0.1 (near-neutral charges) + cls.near_neutral_filler = owl_datatype_min_max_inclusive_restriction(-0.1, 0.1) + + def test_min_cardinality_1_near_neutral_charge(self): + """Min(1, charge, -0.1<=charge<=0.1) counts atoms with near-neutral charge.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.near_neutral_filler) + result = set(self.reasoner.instances(ce)) + # Should equal OWLDataSomeValuesFrom with the same range restriction + svf = OWLDataSomeValuesFrom(property=self.charge_dp, filler=self.near_neutral_filler) + svf_result = set(self.reasoner.instances(svf)) + self.assertEqual(result, svf_result) + self.assertGreater(len(result), 0) + + def test_max_cardinality_0_near_neutral_is_complement_of_min1(self): + """Max(0, charge, -0.1<=c<=0.1) == all - Min(1, charge, -0.1<=c<=0.1).""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.near_neutral_filler) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.near_neutral_filler) + min1_result = set(self.reasoner.instances(min1_ce)) + max0_result = set(self.reasoner.instances(max0_ce)) + self.assertEqual(max0_result, self.all_inds - min1_result) + + def test_exact_cardinality_1_near_neutral_equals_min1(self): + """Exact(1, charge, range) == Min(1, charge, range) when no atom has 2+ matching values.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.near_neutral_filler) + exact1_ce = OWLDataExactCardinality(cardinality=1, property=self.charge_dp, + filler=self.near_neutral_filler) + self.assertEqual(set(self.reasoner.instances(min1_ce)), + set(self.reasoner.instances(exact1_ce))) + + def test_min1_and_max0_near_neutral_cover_all(self): + """Min(1) ∪ Max(0) covers all individuals for any filler.""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.charge_dp, + filler=self.near_neutral_filler) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.charge_dp, + filler=self.near_neutral_filler) + self.assertEqual(set(self.reasoner.instances(min1_ce)) | + set(self.reasoner.instances(max0_ce)), + self.all_inds) + + +class TestDataCardinalityRestrictionsWithNoCacheReasoner(unittest.TestCase): + """ + Same tests but with property_cache=False to exercise the non-cached code paths. + Uses only `lumo` to keep runtime acceptable with the non-cached reasoner. + """ + + @classmethod + def setUpClass(cls): + cls.onto = Ontology(ONTOLOGY_PATH) + # Disable caches to exercise the non-cached branch + cls.reasoner = StructuralReasoner(cls.onto, property_cache=False, class_cache=False) + cls.all_inds = frozenset(cls.onto.individuals_in_signature()) + + cls.lumo_dp = OWLDataProperty(IRI(NS, "lumo")) + cls.double_type = OWLDatatype(XSDVocabulary.DOUBLE) + cls.lumo_filler = owl_datatype_min_inclusive_restriction(-1.5) + + def test_min_cardinality_1_lumo_no_cache(self): + """Min(1, lumo, xsd:double) without cache returns the same count as with cache.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_LUMO) + + def test_min_cardinality_2_lumo_no_cache_is_empty(self): + """Min(2, lumo, xsd:double) without cache should be empty.""" + ce = OWLDataMinCardinality(cardinality=2, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), 0) + + def test_exact_cardinality_1_lumo_no_cache(self): + """Exact(1, lumo, xsd:double) without cache should match all compounds with a lumo value.""" + ce = OWLDataExactCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + self.assertEqual(len(result), INDIVIDUALS_WITH_LUMO) + + def test_max_cardinality_0_lumo_no_cache_count(self): + """Max(0, lumo, xsd:double) without cache returns individuals without a lumo value.""" + ce = OWLDataMaxCardinality(cardinality=0, property=self.lumo_dp, + filler=self.double_type) + result = set(self.reasoner.instances(ce)) + expected = TOTAL_INDIVIDUALS - INDIVIDUALS_WITH_LUMO + self.assertEqual(len(result), expected) + + def test_min1_max0_lumo_cover_all_no_cache(self): + """Min(1, lumo, double) ∪ Max(0, lumo, double) == all individuals (no-cache).""" + min1_ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.double_type) + max0_ce = OWLDataMaxCardinality(cardinality=0, property=self.lumo_dp, + filler=self.double_type) + self.assertEqual(set(self.reasoner.instances(min1_ce)) | + set(self.reasoner.instances(max0_ce)), + self.all_inds) + + def test_min_cardinality_1_lumo_restriction_no_cache(self): + """Min(1, lumo, lumo>=-1.5) without cache equals OWLDataSomeValuesFrom result.""" + ce = OWLDataMinCardinality(cardinality=1, property=self.lumo_dp, + filler=self.lumo_filler) + svf = OWLDataSomeValuesFrom(property=self.lumo_dp, filler=self.lumo_filler) + self.assertEqual(set(self.reasoner.instances(ce)), + set(self.reasoner.instances(svf))) + + +if __name__ == "__main__": + unittest.main() +