1use crate::{
2 BottomUpTa, DetBottomUpTa, FxHashMap, FxHashSet, Symbol,
3 homomorphism::{HomLabel, HomTerm, Homomorphism},
4 run::cartesian_product,
5 traits::{CondensedTa, CondensedTopDownTa, StateUniverse, SymbolSet, TopDownTa},
6};
7use packed_term_arena::tree::TreeArena;
8use smallvec::SmallVec;
9
10pub struct InvHom<'h, A> {
20 inner: A,
21 hom: &'h Homomorphism,
22}
23
24impl<'h, A> InvHom<'h, A> {
25 pub fn new(inner: A, hom: &'h Homomorphism) -> Self {
27 Self { inner, hom }
28 }
29
30 pub fn inner(&self) -> &A {
32 &self.inner
33 }
34
35 pub fn homomorphism(&self) -> &Homomorphism {
37 self.hom
38 }
39}
40
41fn eval_term<A: BottomUpTa>(
42 arena: &TreeArena<HomLabel>,
43 term: HomTerm,
44 src_children: &[A::State],
45 inner: &A,
46 out: &mut dyn FnMut(A::State),
47) {
48 match *arena.get_label(term) {
49 HomLabel::Var(i) => {
50 if let Some(q) = src_children.get(i) {
51 out(q.clone());
52 }
53 }
54 HomLabel::Symbol(symbol) => {
55 let term_children = arena.get_children(term);
56 if term_children.is_empty() {
57 inner.step(symbol, &[], out);
58 return;
59 }
60
61 let mut child_states: SmallVec<[SmallVec<[A::State; 2]>; 4]> = SmallVec::new();
62 for &child in term_children {
63 let mut states = SmallVec::new();
64 eval_term(arena, child, src_children, inner, &mut |q| states.push(q));
65 if states.is_empty() {
66 return;
67 }
68 child_states.push(states);
69 }
70
71 let slices: SmallVec<[&[A::State]; 4]> = child_states
72 .iter()
73 .map(|states| states.as_slice())
74 .collect();
75 cartesian_product(&slices, |combo| inner.step(symbol, combo, out));
76 }
77 }
78}
79
80fn eval_term_det<A: DetBottomUpTa>(
81 arena: &TreeArena<HomLabel>,
82 term: HomTerm,
83 src_children: &[A::State],
84 inner: &A,
85) -> Option<A::State> {
86 match *arena.get_label(term) {
87 HomLabel::Var(i) => src_children.get(i).cloned(),
88 HomLabel::Symbol(symbol) => {
89 let mut combo = SmallVec::<[A::State; 4]>::new();
90 for &child in arena.get_children(term) {
91 combo.push(eval_term_det(arena, child, src_children, inner)?);
92 }
93 inner.step_det(symbol, &combo)
94 }
95 }
96}
97
98impl<A: BottomUpTa> BottomUpTa for InvHom<'_, A> {
99 type State = A::State;
100
101 fn step(&self, f_src: Symbol, children: &[A::State], out: &mut dyn FnMut(A::State)) {
102 let Some(term) = self.hom.get(f_src) else {
103 return;
104 };
105
106 let mut seen = FxHashSet::default();
107 eval_term(self.hom.arena(), term, children, &self.inner, &mut |q| {
108 if seen.insert(q.clone()) {
109 out(q);
110 }
111 });
112 }
113
114 fn is_accepting(&self, q: &A::State) -> bool {
115 self.inner.is_accepting(q)
116 }
117}
118
119impl<A: DetBottomUpTa> DetBottomUpTa for InvHom<'_, A> {
120 fn step_det(&self, f_src: Symbol, children: &[A::State]) -> Option<A::State> {
121 let term = self.hom.get(f_src)?;
122 eval_term_det(self.hom.arena(), term, children, &self.inner)
123 }
124
125 fn det_group(&self, f_src: Symbol) -> u32 {
131 self.hom.term_id(f_src).map_or(u32::MAX, |tid| tid as u32)
132 }
133}
134
135impl<A: StateUniverse> StateUniverse for InvHom<'_, A> {
136 fn all_states(&self, out: &mut dyn FnMut(A::State)) {
137 self.inner.all_states(out);
138 }
139}
140
141#[derive(Clone, Debug)]
142struct InnerCondensedRule<S> {
143 children: Vec<S>,
144 symbols: SymbolSet,
145 result: S,
146}
147
148#[derive(Clone, Debug)]
149struct PartialEval<S> {
150 assignments: Vec<Option<S>>,
151 result: S,
152}
153
154#[derive(Clone, Debug)]
155struct DirectTerm {
156 symbol: Symbol,
157 variables: Vec<usize>,
158}
159
160fn direct_linear_term(
161 arena: &TreeArena<HomLabel>,
162 term: HomTerm,
163 arity: usize,
164) -> Option<DirectTerm> {
165 let HomLabel::Symbol(symbol) = *arena.get_label(term) else {
166 return None;
167 };
168
169 let mut seen = vec![false; arity];
170 let mut variables = Vec::new();
171 for &child in arena.get_children(term) {
172 let HomLabel::Var(variable) = *arena.get_label(child) else {
173 return None;
174 };
175 if variable >= arity || seen[variable] {
176 return None;
177 }
178 seen[variable] = true;
179 variables.push(variable);
180 }
181
182 Some(DirectTerm { symbol, variables })
183}
184
185#[allow(clippy::type_complexity)]
186fn match_topdown_term<A>(
187 arena: &TreeArena<HomLabel>,
188 term: HomTerm,
189 state: &A::State,
190 arity: usize,
191 inner: &A,
192 subst: &mut [Option<A::State>],
193 out: &mut dyn FnMut(&mut [Option<A::State>]),
194) where
195 A: TopDownTa,
196{
197 match *arena.get_label(term) {
198 HomLabel::Var(variable) => {
199 if variable >= arity {
200 return;
201 }
202
203 match &subst[variable] {
204 Some(existing) if existing == state => out(subst),
205 Some(_) => {}
206 None => {
207 subst[variable] = Some(state.clone());
208 out(subst);
209 subst[variable] = None;
210 }
211 }
212 }
213 HomLabel::Symbol(symbol) => {
214 let term_children = arena.get_children(term);
215 inner.step_topdown(state, &mut |rule_symbol, rule_children| {
216 if rule_symbol != symbol || rule_children.len() != term_children.len() {
217 return;
218 }
219 match_topdown_children(
220 arena,
221 term_children,
222 rule_children,
223 arity,
224 inner,
225 subst,
226 0,
227 out,
228 );
229 });
230 }
231 }
232}
233
234#[allow(clippy::too_many_arguments, clippy::type_complexity)]
235fn match_topdown_children<A>(
236 arena: &TreeArena<HomLabel>,
237 term_children: &[HomTerm],
238 rule_children: &[A::State],
239 arity: usize,
240 inner: &A,
241 subst: &mut [Option<A::State>],
242 position: usize,
243 out: &mut dyn FnMut(&mut [Option<A::State>]),
244) where
245 A: TopDownTa,
246{
247 if position == term_children.len() {
248 out(subst);
249 return;
250 }
251
252 match_topdown_term(
253 arena,
254 term_children[position],
255 &rule_children[position],
256 arity,
257 inner,
258 subst,
259 &mut |subst| {
260 match_topdown_children(
261 arena,
262 term_children,
263 rule_children,
264 arity,
265 inner,
266 subst,
267 position + 1,
268 out,
269 );
270 },
271 );
272}
273
274fn emit_if_complete<S: Clone>(
275 subst: &[Option<S>],
276 children_scratch: &mut SmallVec<[S; 4]>,
277 symbols: &SymbolSet,
278 out: &mut dyn FnMut(&SymbolSet, &[S]),
279) {
280 children_scratch.clear();
281 for state in subst {
282 let Some(state) = state else {
283 children_scratch.clear();
284 return;
285 };
286 children_scratch.push(state.clone());
287 }
288 out(symbols, children_scratch);
289}
290
291fn merge_assignments<S: Clone + Eq>(
292 left: &[Option<S>],
293 right: &[Option<S>],
294) -> Option<Vec<Option<S>>> {
295 let mut merged = left.to_vec();
296 for (idx, value) in right.iter().enumerate() {
297 let Some(value) = value else {
298 continue;
299 };
300 match &merged[idx] {
301 Some(existing) if existing != value => return None,
302 Some(_) => {}
303 None => merged[idx] = Some(value.clone()),
304 }
305 }
306 Some(merged)
307}
308
309fn eval_condensed_term<A>(
310 arena: &TreeArena<HomLabel>,
311 term: HomTerm,
312 arity: usize,
313 expected: Option<&A::State>,
314 inner_rules: &[InnerCondensedRule<A::State>],
315 inner: &A,
316) -> Vec<PartialEval<A::State>>
317where
318 A: StateUniverse,
319{
320 match *arena.get_label(term) {
321 HomLabel::Var(variable) => {
322 if variable >= arity {
323 return Vec::new();
324 }
325 let mut out = Vec::new();
326 if let Some(q) = expected {
327 let mut assignments = vec![None; arity];
328 assignments[variable] = Some(q.clone());
329 out.push(PartialEval {
330 assignments,
331 result: q.clone(),
332 });
333 } else {
334 inner.all_states(&mut |q| {
335 let mut assignments = vec![None; arity];
336 assignments[variable] = Some(q.clone());
337 out.push(PartialEval {
338 assignments,
339 result: q,
340 });
341 });
342 }
343 out
344 }
345 HomLabel::Symbol(symbol) => {
346 let term_children = arena.get_children(term);
347 let mut out = Vec::new();
348
349 for rule in inner_rules {
350 if !rule.symbols.contains(symbol) {
351 continue;
352 }
353 if rule.children.len() != term_children.len() {
354 continue;
355 }
356 if let Some(q) = expected
357 && &rule.result != q
358 {
359 continue;
360 }
361
362 let mut partials = vec![vec![None; arity]];
363 for (&child_term, child_state) in term_children.iter().zip(&rule.children) {
364 let child_evals = eval_condensed_term(
365 arena,
366 child_term,
367 arity,
368 Some(child_state),
369 inner_rules,
370 inner,
371 );
372 if child_evals.is_empty() {
373 partials.clear();
374 break;
375 }
376
377 let mut next = Vec::new();
378 for partial in &partials {
379 for child_eval in &child_evals {
380 if let Some(merged) =
381 merge_assignments(partial, &child_eval.assignments)
382 {
383 next.push(merged);
384 }
385 }
386 }
387 partials = next;
388 if partials.is_empty() {
389 break;
390 }
391 }
392
393 for assignments in partials {
394 out.push(PartialEval {
395 assignments,
396 result: rule.result.clone(),
397 });
398 }
399 }
400
401 out
402 }
403 }
404}
405
406fn collect_inner_condensed_rules<A: CondensedTa>(inner: &A) -> Vec<InnerCondensedRule<A::State>> {
407 let mut inner_rules = Vec::new();
408 inner.condensed_rules(&mut |children, symbols, result| {
409 inner_rules.push(InnerCondensedRule {
410 children: children.to_vec(),
411 symbols: symbols.clone(),
412 result,
413 });
414 });
415 inner_rules
416}
417
418impl<A> CondensedTa for InvHom<'_, A>
419where
420 A: CondensedTa + StateUniverse,
421{
422 fn condensed_rules(&self, out: &mut dyn FnMut(&[A::State], &SymbolSet, A::State)) {
423 let inner_rules = collect_inner_condensed_rules(&self.inner);
424 let mut inner_by_symbol: FxHashMap<Symbol, Vec<usize>> = FxHashMap::default();
425 for (idx, rule) in inner_rules.iter().enumerate() {
426 for symbol in rule.symbols.iter() {
427 inner_by_symbol.entry(symbol).or_default().push(idx);
428 }
429 }
430
431 let mut groups: FxHashMap<(Vec<A::State>, A::State), SymbolSet> = FxHashMap::default();
432 for (term_id, labels, term) in self.hom.term_sets() {
433 let Some(&first_label) = labels.first() else {
434 continue;
435 };
436 let Some(arity) = self.hom.source_arity(first_label) else {
437 continue;
438 };
439
440 if let Some(direct) = direct_linear_term(self.hom.arena(), term, arity) {
441 if let Some(rule_indexes) = inner_by_symbol.get(&direct.symbol) {
442 for &rule_idx in rule_indexes {
443 let rule = &inner_rules[rule_idx];
444 if rule.children.len() != direct.variables.len() {
445 continue;
446 }
447
448 let mut children = vec![None; arity];
449 for (&variable, child) in direct.variables.iter().zip(&rule.children) {
450 children[variable] = Some(child.clone());
451 }
452 let Some(children) = children.into_iter().collect::<Option<Vec<_>>>()
453 else {
454 continue;
455 };
456
457 let sym_set = groups.entry((children, rule.result.clone())).or_default();
458 for &label in self.hom.label_set(term_id) {
459 sym_set.insert(label);
460 }
461 }
462 }
463 continue;
464 }
465
466 let evals = eval_condensed_term(
467 self.hom.arena(),
468 term,
469 arity,
470 None,
471 &inner_rules,
472 &self.inner,
473 );
474 for eval in evals {
475 let Some(children) = eval.assignments.into_iter().collect::<Option<Vec<_>>>()
476 else {
477 continue;
478 };
479 let sym_set = groups.entry((children, eval.result)).or_default();
480 for &label in self.hom.label_set(term_id) {
481 sym_set.insert(label);
482 }
483 }
484 }
485
486 for ((children, result), symbols) in groups {
487 out(&children, &symbols, result);
488 }
489 }
490
491 fn condensed_nullary_rules(&self, out: &mut dyn FnMut(&SymbolSet, A::State)) {
492 let mut fallback = Vec::new();
493 for (term_id, labels, term) in self.hom.term_sets() {
494 let Some(&first_label) = labels.first() else {
495 continue;
496 };
497 let Some(arity) = self.hom.source_arity(first_label) else {
498 continue;
499 };
500 if arity != 0 {
501 continue;
502 }
503
504 let mut source_symbols = SymbolSet::new();
505 for &label in self.hom.label_set(term_id) {
506 source_symbols.insert(label);
507 }
508
509 if let Some(direct) = direct_linear_term(self.hom.arena(), term, arity)
510 && direct.variables.is_empty()
511 {
512 self.inner
513 .condensed_nullary_rules(&mut |inner_symbols, result| {
514 if inner_symbols.contains(direct.symbol) {
515 out(&source_symbols, result);
516 }
517 });
518 continue;
519 }
520
521 fallback.push((source_symbols, term));
522 }
523
524 if !fallback.is_empty() {
525 let inner_rules = collect_inner_condensed_rules(&self.inner);
526 for (symbols, term) in fallback {
527 for eval in
528 eval_condensed_term(self.hom.arena(), term, 0, None, &inner_rules, &self.inner)
529 {
530 if eval.assignments.is_empty() {
531 out(&symbols, eval.result);
532 }
533 }
534 }
535 }
536 }
537
538 fn condensed_rules_by_child(
539 &self,
540 position: usize,
541 state: &A::State,
542 out: &mut dyn FnMut(&[A::State], &SymbolSet, A::State),
543 ) {
544 let mut fallback = Vec::new();
545 for (term_id, labels, term) in self.hom.term_sets() {
546 let Some(&first_label) = labels.first() else {
547 continue;
548 };
549 let Some(arity) = self.hom.source_arity(first_label) else {
550 continue;
551 };
552 if position >= arity {
553 continue;
554 }
555
556 let mut source_symbols = SymbolSet::new();
557 for &label in self.hom.label_set(term_id) {
558 source_symbols.insert(label);
559 }
560
561 let Some(direct) = direct_linear_term(self.hom.arena(), term, arity) else {
562 fallback.push((source_symbols, term, arity));
563 continue;
564 };
565 let Some(inner_position) = direct
566 .variables
567 .iter()
568 .position(|&variable| variable == position)
569 else {
570 continue;
571 };
572
573 self.inner.condensed_rules_by_child(
574 inner_position,
575 state,
576 &mut |inner_children, inner_symbols, result| {
577 if !inner_symbols.contains(direct.symbol)
578 || inner_children.len() != direct.variables.len()
579 {
580 return;
581 }
582
583 let mut children = vec![None; arity];
584 for (&variable, child) in direct.variables.iter().zip(inner_children) {
585 children[variable] = Some(child.clone());
586 }
587 let Some(children) = children.into_iter().collect::<Option<Vec<_>>>() else {
588 return;
589 };
590 out(&children, &source_symbols, result);
591 },
592 );
593 }
594
595 if !fallback.is_empty() {
596 let inner_rules = collect_inner_condensed_rules(&self.inner);
597 for (symbols, term, arity) in fallback {
598 for eval in eval_condensed_term(
599 self.hom.arena(),
600 term,
601 arity,
602 None,
603 &inner_rules,
604 &self.inner,
605 ) {
606 let Some(children) = eval.assignments.into_iter().collect::<Option<Vec<_>>>()
607 else {
608 continue;
609 };
610 if children.get(position) == Some(state) {
611 out(&children, &symbols, eval.result);
612 }
613 }
614 }
615 }
616 }
617}
618
619impl<A> CondensedTopDownTa for InvHom<'_, A>
620where
621 A: TopDownTa,
622{
623 fn condensed_rules_by_parent(
624 &self,
625 parent: &A::State,
626 out: &mut dyn FnMut(&SymbolSet, &[A::State]),
627 ) {
628 let arena = self.hom.arena();
629 let mut source_symbols = SymbolSet::new();
630 let mut subst = SmallVec::<[Option<A::State>; 4]>::new();
631 let mut children_scratch = SmallVec::<[A::State; 4]>::new();
632
633 for (term_id, labels, term) in self.hom.term_sets() {
634 let Some(&first_label) = labels.first() else {
635 continue;
636 };
637 let Some(arity) = self.hom.source_arity(first_label) else {
638 continue;
639 };
640
641 source_symbols.clear();
642 for &label in self.hom.label_set(term_id) {
643 source_symbols.insert(label);
644 }
645
646 subst.clear();
647 subst.resize_with(arity, || None);
648
649 if let Some(direct) = direct_linear_term(arena, term, arity) {
650 self.inner
651 .step_topdown(parent, &mut |target_symbol, target_children| {
652 if target_symbol != direct.symbol
653 || target_children.len() != direct.variables.len()
654 {
655 return;
656 }
657
658 subst.fill(None);
659 for (&variable, child) in direct.variables.iter().zip(target_children) {
660 subst[variable] = Some(child.clone());
661 }
662 emit_if_complete(&subst, &mut children_scratch, &source_symbols, out);
663 });
664 continue;
665 }
666
667 match_topdown_term(
668 arena,
669 term,
670 parent,
671 arity,
672 &self.inner,
673 &mut subst,
674 &mut |subst| {
675 emit_if_complete(subst, &mut children_scratch, &source_symbols, out);
676 },
677 );
678 }
679 }
680
681 fn condensed_initial_states(&self, out: &mut dyn FnMut(A::State)) {
682 self.inner.initial_states(out);
683 }
684}
685
686#[cfg(test)]
687mod tests {
688 use super::*;
689 use crate::{BottomUpTa, DetBottomUpTa, ExplicitBuilder, StateId};
690 use std::cell::Cell;
691
692 fn sym(i: u32) -> Symbol {
693 Symbol(i)
694 }
695
696 fn var(arena: &mut TreeArena<HomLabel>, i: usize) -> HomTerm {
697 arena.add_node(HomLabel::Var(i), vec![])
698 }
699
700 fn node(arena: &mut TreeArena<HomLabel>, symbol: Symbol, children: Vec<HomTerm>) -> HomTerm {
701 arena.add_node(HomLabel::Symbol(symbol), children)
702 }
703
704 fn make_inner() -> (crate::Explicit, StateId, StateId, StateId) {
705 let mut b = ExplicitBuilder::new();
706 let q0 = b.new_state();
707 let q1 = b.new_state();
708 let qr = b.new_state();
709 b.add_rule(sym(10), vec![q0, q1], qr);
710 b.add_accepting(qr);
711 (b.build(), q0, q1, qr)
712 }
713
714 #[test]
715 fn depth1_step_delegates_to_inner() {
716 let (inner, q0, q1, qr) = make_inner();
717 let mut arena = TreeArena::new();
718 let v0 = var(&mut arena, 0);
719 let v1 = var(&mut arena, 1);
720 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
721 let mut hom = Homomorphism::with_arena(arena);
722 hom.add(sym(0), 2, rhs).unwrap();
723 let inv = InvHom::new(inner, &hom);
724
725 let mut out = Vec::new();
726 inv.step(sym(0), &[q0, q1], &mut |q| out.push(q));
727 assert_eq!(out, vec![qr]);
728 assert!(inv.is_accepting(&qr));
729 }
730
731 #[test]
732 fn step_deduplicates_results() {
733 #[derive(Clone)]
734 struct DuplicateInner;
735
736 impl BottomUpTa for DuplicateInner {
737 type State = StateId;
738
739 fn step(&self, _f: Symbol, _children: &[StateId], out: &mut dyn FnMut(StateId)) {
740 out(StateId(7));
741 out(StateId(7));
742 }
743
744 fn is_accepting(&self, _q: &StateId) -> bool {
745 false
746 }
747 }
748
749 let mut arena = TreeArena::new();
750 let v0 = var(&mut arena, 0);
751 let rhs = node(&mut arena, sym(10), vec![v0]);
752 let mut hom = Homomorphism::with_arena(arena);
753 hom.add(sym(0), 1, rhs).unwrap();
754 let inv = InvHom::new(DuplicateInner, &hom);
755
756 let mut out = Vec::new();
757 inv.step(sym(0), &[StateId(0)], &mut |q| out.push(q));
758 assert_eq!(out, vec![StateId(7)]);
759 }
760
761 #[test]
762 fn depth1_step_det_delegates_to_inner() {
763 let (inner, q0, q1, qr) = make_inner();
764 let mut arena = TreeArena::new();
765 let v0 = var(&mut arena, 0);
766 let v1 = var(&mut arena, 1);
767 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
768 let mut hom = Homomorphism::with_arena(arena);
769 hom.add(sym(0), 2, rhs).unwrap();
770 let inv = InvHom::new(inner, &hom);
771 assert_eq!(inv.step_det(sym(0), &[q0, q1]), Some(qr));
772 assert_eq!(inv.step_det(sym(0), &[q1, q0]), None);
773 }
774
775 #[test]
776 fn unmapped_symbol_emits_nothing() {
777 let (inner, q0, q1, _qr) = make_inner();
778 let arena = TreeArena::new();
779 let hom = Homomorphism::with_arena(arena);
780 let inv = InvHom::new(inner, &hom);
781 let mut out = Vec::new();
782 inv.step(sym(99), &[q0, q1], &mut |q| out.push(q));
783 assert!(out.is_empty());
784 }
785
786 #[test]
787 fn nullary_ground_term_evaluates_correctly() {
788 let mut b = ExplicitBuilder::new();
789 let qa = b.new_state();
790 b.add_rule(sym(20), vec![], qa);
791 b.add_accepting(qa);
792 let inner = b.build();
793
794 let mut arena = TreeArena::new();
795 let rhs = node(&mut arena, sym(20), vec![]);
796 let mut hom = Homomorphism::with_arena(arena);
797 hom.add(sym(0), 0, rhs).unwrap();
798 let inv = InvHom::new(inner, &hom);
799
800 let mut out = Vec::new();
801 inv.step(sym(0), &[], &mut |q| out.push(q));
802 assert_eq!(out, vec![qa]);
803 assert!(inv.is_accepting(&qa));
804 }
805
806 #[test]
807 fn depth2_term_evaluates_correctly() {
808 let mut b = ExplicitBuilder::new();
809 let q_leaf = b.new_state();
810 let q_inner = b.new_state();
811 let q1 = b.new_state();
812 let qr = b.new_state();
813 b.add_rule(sym(5), vec![q_leaf], q_inner);
814 b.add_rule(sym(6), vec![q_inner, q1], qr);
815 b.add_accepting(qr);
816 let inner = b.build();
817
818 let mut arena = TreeArena::new();
819 let wrapped_v0 = var(&mut arena, 0);
820 let wrapped = node(&mut arena, sym(5), vec![wrapped_v0]);
821 let v1 = var(&mut arena, 1);
822 let rhs = node(&mut arena, sym(6), vec![wrapped, v1]);
823 let mut hom = Homomorphism::with_arena(arena);
824 hom.add(sym(0), 2, rhs).unwrap();
825 let inv = InvHom::new(inner, &hom);
826
827 let mut out = Vec::new();
828 inv.step(sym(0), &[q_leaf, q1], &mut |q| out.push(q));
829 assert_eq!(out, vec![qr]);
830 }
831
832 #[test]
833 fn condensed_depth1_groups_source_symbols() {
834 let (inner, q0, q1, qr) = make_inner();
835 let mut arena = TreeArena::new();
836 let v0 = var(&mut arena, 0);
837 let v1 = var(&mut arena, 1);
838 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
839 let same_v0 = var(&mut arena, 0);
840 let same_v1 = var(&mut arena, 1);
841 let same = node(&mut arena, sym(10), vec![same_v0, same_v1]);
842 let mut hom = Homomorphism::with_arena(arena);
843 hom.add(sym(0), 2, rhs).unwrap();
844 hom.add(sym(1), 2, same).unwrap();
845 let inv = InvHom::new(inner, &hom);
846
847 let mut groups = Vec::new();
848 inv.condensed_rules(&mut |children, symbols, result| {
849 groups.push((children.to_vec(), symbols.clone(), result));
850 });
851
852 assert_eq!(groups.len(), 1);
853 assert_eq!(groups[0].0, vec![q0, q1]);
854 assert!(groups[0].1.contains(sym(0)));
855 assert!(groups[0].1.contains(sym(1)));
856 assert_eq!(groups[0].2, qr);
857 }
858
859 #[test]
860 fn indexed_condensed_depth1_uses_hom_label_sets() {
861 let (inner, q0, q1, qr) = make_inner();
862 let mut arena = TreeArena::new();
863 let v0 = var(&mut arena, 0);
864 let v1 = var(&mut arena, 1);
865 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
866 let same_v0 = var(&mut arena, 0);
867 let same_v1 = var(&mut arena, 1);
868 let same = node(&mut arena, sym(10), vec![same_v0, same_v1]);
869 let mut hom = Homomorphism::with_arena(arena);
870 hom.add(sym(0), 2, rhs).unwrap();
871 hom.add(sym(1), 2, same).unwrap();
872 let inv = InvHom::new(inner, &hom);
873
874 let mut groups = Vec::new();
875 inv.condensed_rules_by_child(0, &q0, &mut |children, symbols, result| {
876 groups.push((children.to_vec(), symbols.clone(), result));
877 });
878
879 assert_eq!(groups.len(), 1);
880 assert_eq!(groups[0].0, vec![q0, q1]);
881 assert!(groups[0].1.contains(sym(0)));
882 assert!(groups[0].1.contains(sym(1)));
883 assert_eq!(groups[0].2, qr);
884 }
885
886 #[test]
887 fn topdown_condensed_depth1_uses_hom_label_sets() {
888 let (inner, q0, q1, qr) = make_inner();
889 let mut arena = TreeArena::new();
890 let v0 = var(&mut arena, 0);
891 let v1 = var(&mut arena, 1);
892 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
893 let same_v0 = var(&mut arena, 0);
894 let same_v1 = var(&mut arena, 1);
895 let same = node(&mut arena, sym(10), vec![same_v0, same_v1]);
896 let mut hom = Homomorphism::with_arena(arena);
897 hom.add(sym(0), 2, rhs).unwrap();
898 hom.add(sym(1), 2, same).unwrap();
899 let inv = InvHom::new(inner, &hom);
900
901 let mut groups = Vec::new();
902 inv.condensed_rules_by_parent(&qr, &mut |symbols, children| {
903 groups.push((children.to_vec(), symbols.clone()));
904 });
905
906 assert_eq!(groups.len(), 1);
907 assert_eq!(groups[0].0, vec![q0, q1]);
908 assert!(groups[0].1.contains(sym(0)));
909 assert!(groups[0].1.contains(sym(1)));
910 }
911
912 #[test]
913 fn condensed_nested_rhs_matches_step_enumeration() {
914 let mut b = ExplicitBuilder::new();
915 let q_leaf = b.new_state();
916 let q_inner = b.new_state();
917 let q1 = b.new_state();
918 let qr = b.new_state();
919 b.add_rule(sym(5), vec![q_leaf], q_inner);
920 b.add_rule(sym(6), vec![q_inner, q1], qr);
921 let inner = b.build();
922
923 let mut arena = TreeArena::new();
924 let wrapped_v0 = var(&mut arena, 0);
925 let wrapped = node(&mut arena, sym(5), vec![wrapped_v0]);
926 let v1 = var(&mut arena, 1);
927 let rhs = node(&mut arena, sym(6), vec![wrapped, v1]);
928 let mut hom = Homomorphism::with_arena(arena);
929 hom.add(sym(0), 2, rhs).unwrap();
930 let inv = InvHom::new(inner, &hom);
931
932 let mut condensed = Vec::new();
933 inv.condensed_rules(&mut |children, symbols, result| {
934 for src in symbols.iter() {
935 condensed.push((src, children.to_vec(), result));
936 }
937 });
938
939 let mut stepped = Vec::new();
940 inv.step(sym(0), &[q_leaf, q1], &mut |q| {
941 stepped.push((sym(0), vec![q_leaf, q1], q));
942 });
943 condensed.sort();
944 stepped.sort();
945 assert_eq!(condensed, stepped);
946 }
947
948 #[test]
949 fn topdown_condensed_nested_rhs_streams_matches() {
950 let mut b = ExplicitBuilder::new();
951 let q_leaf = b.new_state();
952 let q_inner = b.new_state();
953 let q1 = b.new_state();
954 let qr = b.new_state();
955 b.add_rule(sym(5), vec![q_leaf], q_inner);
956 b.add_rule(sym(6), vec![q_inner, q1], qr);
957 let inner = b.build();
958
959 let mut arena = TreeArena::new();
960 let wrapped_v0 = var(&mut arena, 0);
961 let wrapped = node(&mut arena, sym(5), vec![wrapped_v0]);
962 let v1 = var(&mut arena, 1);
963 let rhs = node(&mut arena, sym(6), vec![wrapped, v1]);
964 let mut hom = Homomorphism::with_arena(arena);
965 hom.add(sym(0), 2, rhs).unwrap();
966 let inv = InvHom::new(inner, &hom);
967
968 let mut groups = Vec::new();
969 inv.condensed_rules_by_parent(&qr, &mut |symbols, children| {
970 groups.push((children.to_vec(), symbols.clone()));
971 });
972
973 assert_eq!(groups.len(), 1);
974 assert_eq!(groups[0].0, vec![q_leaf, q1]);
975 assert!(groups[0].1.contains(sym(0)));
976 }
977
978 #[test]
979 fn condensed_supports_ground_subterms() {
980 let mut b = ExplicitBuilder::new();
981 let qa = b.new_state();
982 let qx = b.new_state();
983 let qr = b.new_state();
984 b.add_rule(sym(3), vec![], qa);
985 b.add_rule(sym(4), vec![qa, qx], qr);
986 let inner = b.build();
987
988 let mut arena = TreeArena::new();
989 let ground = node(&mut arena, sym(3), vec![]);
990 let v0 = var(&mut arena, 0);
991 let rhs = node(&mut arena, sym(4), vec![ground, v0]);
992 let mut hom = Homomorphism::with_arena(arena);
993 hom.add(sym(0), 1, rhs).unwrap();
994 let inv = InvHom::new(inner, &hom);
995
996 let mut groups = Vec::new();
997 inv.condensed_rules(&mut |children, symbols, result| {
998 groups.push((children.to_vec(), symbols.clone(), result));
999 });
1000
1001 assert_eq!(groups.len(), 1);
1002 assert_eq!(groups[0].0, vec![qx]);
1003 assert!(groups[0].1.contains(sym(0)));
1004 assert_eq!(groups[0].2, qr);
1005 }
1006
1007 #[test]
1008 fn condensed_supports_bare_variable_rhs() {
1009 let mut b = ExplicitBuilder::new();
1010 let q0 = b.new_state();
1011 let q1 = b.new_state();
1012 b.add_rule(sym(10), vec![], q0);
1013 b.add_rule(sym(11), vec![], q1);
1014 let inner = b.build();
1015
1016 let mut arena = TreeArena::new();
1017 let rhs = var(&mut arena, 0);
1018 let mut hom = Homomorphism::with_arena(arena);
1019 hom.add(sym(0), 1, rhs).unwrap();
1020 let inv = InvHom::new(inner, &hom);
1021
1022 let mut groups = Vec::new();
1023 inv.condensed_rules(&mut |children, symbols, result| {
1024 groups.push((children.to_vec(), symbols.clone(), result));
1025 });
1026 groups.sort_by_key(|(children, _, result)| (children.clone(), *result));
1027
1028 assert_eq!(groups.len(), 2);
1029 assert_eq!(groups[0].0, vec![q0]);
1030 assert_eq!(groups[0].2, q0);
1031 assert!(groups[0].1.contains(sym(0)));
1032 assert_eq!(groups[1].0, vec![q1]);
1033 assert_eq!(groups[1].2, q1);
1034 assert!(groups[1].1.contains(sym(0)));
1035 }
1036
1037 #[test]
1038 fn condensed_constrained_variables_do_not_enumerate_universe() {
1039 struct CountingInner {
1040 all_states_calls: Cell<usize>,
1041 }
1042
1043 impl BottomUpTa for CountingInner {
1044 type State = u8;
1045
1046 fn step(&self, _f: Symbol, _children: &[u8], _out: &mut dyn FnMut(u8)) {}
1047
1048 fn is_accepting(&self, q: &u8) -> bool {
1049 *q == 2
1050 }
1051 }
1052
1053 impl StateUniverse for CountingInner {
1054 fn all_states(&self, _out: &mut dyn FnMut(u8)) {
1055 self.all_states_calls.set(self.all_states_calls.get() + 1);
1056 }
1057 }
1058
1059 impl CondensedTa for CountingInner {
1060 fn condensed_rules(&self, out: &mut dyn FnMut(&[u8], &SymbolSet, u8)) {
1061 let mut symbols = SymbolSet::new();
1062 symbols.insert(sym(10));
1063 out(&[0, 1], &symbols, 2);
1064 }
1065 }
1066
1067 let inner = CountingInner {
1068 all_states_calls: Cell::new(0),
1069 };
1070 let mut arena = TreeArena::new();
1071 let v0 = var(&mut arena, 0);
1072 let v1 = var(&mut arena, 1);
1073 let rhs = node(&mut arena, sym(10), vec![v0, v1]);
1074 let mut hom = Homomorphism::with_arena(arena);
1075 hom.add(sym(0), 2, rhs).unwrap();
1076 let inv = InvHom::new(inner, &hom);
1077
1078 let mut rules = Vec::new();
1079 inv.condensed_rules(&mut |children, symbols, result| {
1080 rules.push((children.to_vec(), symbols.clone(), result));
1081 });
1082
1083 assert_eq!(rules.len(), 1);
1084 assert_eq!(rules[0].0, vec![0, 1]);
1085 assert_eq!(rules[0].2, 2);
1086 assert_eq!(inv.inner().all_states_calls.get(), 0);
1087 }
1088}