Struct QueryRewriter 

pub struct QueryRewriter { /* private fields */ }

The PerfectRef query rewriter for OWL 2 QL

Extended to handle union query rewriting (ObjectUnionOf on RHS of SubClassOf).

Implementations

impl QueryRewriter

pub fn new(tbox: Owl2QLTBox) -> Self

Create a new rewriter with a classified TBox

pub fn with_limit(tbox: Owl2QLTBox, max_rewrites: usize) -> Self

Create with a custom rewriting limit

pub fn tbox(&self) -> &Owl2QLTBox

Access the underlying TBox

pub fn rewrite_query( &self, query: &ConjunctiveQuery, ) -> Result<RewrittenQuery, QlError>

Main entry point: rewrite a conjunctive query using PerfectRef algorithm.

Returns a RewrittenQuery (UCQ) that is equivalent to the original CQ over any ABox consistent with the TBox.

This extended version handles:

• Standard subclass/subproperty/domain/range unfolding
• Union axiom branching: C ⊑ A ⊔ B causes the type atom ?x:A to gain an additional CQ branch where ?x:C replaces the atom (since C individuals that are A will satisfy the query).

pub fn unfold_atom(&self, atom: &QueryAtom) -> Vec<QueryAtom>

Unfold a single query atom using TBox axioms. Returns all possible alternative atoms (including the original).

pub fn unfold_type_atom_union_branches( &self, individual: &QueryTerm, class: &str, ) -> Vec<QueryAtom>

Compute additional type atom alternatives arising from union axioms.

For a type atom ?x:A, if there is a union axiom C ⊑ A ⊔ B, then C individuals that happen to be A will satisfy the query. We cannot replace ?x:A with ?x:C (since not all C are A), but we can add a branch that queries ?x:C with the understanding that a C that is not B must be A (by the closed-world assumption on the union).

In the PerfectRef framework for OWL 2 QL, union rewriting produces new CQ branches where the type atom is replaced by the sub-concept C (the class that is subsumed by the union). This is correct because:

• If ?x is a C individual and C ⊑ A ⊔ B, then ?x satisfies A or B.
• The query ?x:A is satisfied if we can certify ?x is a C that is an A.

Returns a list of replacement atoms (one per union branch sub-concept).

pub fn is_satisfiable(&self, class: &str) -> bool

Check if a class assertion is trivially satisfiable given the TBox

pub fn rewrite_query_union_aware( &self, query: &ConjunctiveQuery, ) -> Result<RewrittenQuery, QlError>

Compute union-aware query rewriting for a conjunctive query where union axioms guide query branching.

This method extends rewrite_query by explicitly computing all union disjunct branches for each type atom and emitting separate CQs for each possible branch derivation path.

For example, given: TBox: Dog ⊑ Animal ⊔ Pet Query: ?x:Animal

The rewriting includes: ?x:Animal (original) ?x:Dog (from union: Dog may be an Animal)

pub fn union_siblings_for(&self, class: &str) -> Vec<Vec<String>>

Compute all union disjunct branches for a named class.

Returns a list of lists — each inner list is a set of class names that are sibling disjuncts in some union axiom where class participates.

Example: if TBox contains C ⊑ A ⊔ B, then: union_siblings_for(“A”) → [[“A”, “B”]]

pub fn are_union_siblings(&self, class_a: &str, class_b: &str) -> bool

Check if class A and class B are in a union axiom together (sibling disjuncts)

pub fn conjunction_satisfiable(&self, classes: &[&str]) -> bool

Compute satisfiability of a concept conjunction {C₁, C₂, …} w.r.t. the TBox.

Returns false if the conjunction is definitely unsatisfiable based on:

• Direct disjointness between any two members
• Union axiom exhaustion: C ⊑ A ⊔ B and neither A nor B is compatible