fn rewrite(&mut self, t: DataExpression) -> DataExpression {

        let mut stats = RewritingStatistics::default();

        trace!("input: {}", t);

        let result = InnermostRewriter::rewrite_aux(

            &mut self.tp.borrow_mut(),

            &mut self.stack,

            &mut self.builder,

            &mut stats,

            &self.apma,

            t,

        );

        info!(

            "{} rewrites, {} single steps and {} symbol comparisons",

        result

    }

    pub fn new(tp: Rc<RefCell<TermPool>>, spec: &RewriteSpecification) -> InnermostRewriter {

        let apma = SetAutomaton::new(spec, AnnouncementInnermost::new, true);

        info!("ATerm pool: {}", tp.borrow());

        InnermostRewriter {

            apma,

            tp: tp.clone(),

            stack: InnermostStack::default(),

            builder: SCCTBuilder::new(),

        }

    }

    pub(crate) fn rewrite_aux(

        tp: &mut TermPool,

        stack: &mut InnermostStack,

        builder: &mut SCCTBuilder,

        stats: &mut RewritingStatistics,

        automaton: &SetAutomaton<AnnouncementInnermost>,

        input_term: DataExpression,

    ) -> DataExpression {

        debug_assert!(!input_term.is_default(), "Cannot rewrite the default term");

        stats.recursions += 1;

        {

            let mut write_terms = stack.terms.write();

            let mut write_configs = stack.configs.write();

            // Push the result term to the stack.

            let top_of_stack = write_terms.len();

            write_configs.push(Config::Return());

            write_terms.push(DataExpressionRef::default());

            InnermostStack::add_rewrite(&mut write_configs, &mut write_terms, input_term.copy(), top_of_stack);

        }

            trace!("{}", stack);

            let mut write_configs = stack.configs.write();

            if let Some(config) = write_configs.pop() {

                match config {

                    Config::Rewrite(result) => {

                        let mut write_terms = stack.terms.write();

                        let term = write_terms.pop().unwrap();

                        let symbol = term.data_function_symbol();

                        let arguments = term.data_arguments();

                        // For all the argument we reserve space on the stack.

                        let top_of_stack = write_terms.len();

                        for _ in 0..arguments.len() {

                            write_terms.push(Default::default());

                        }

                        let symbol = write_configs.protect(&symbol.into());

                        InnermostStack::add_result(&mut write_configs, symbol.into(), arguments.len(), result);

                        for (offset, arg) in arguments.into_iter().enumerate() {

                            InnermostStack::add_rewrite(

                                &mut write_configs,

                                &mut write_terms,

                                arg.into(),

                                top_of_stack + offset,

                            );

                        }

                        drop(write_configs);

                    Config::Construct(symbol, arity, index) => {

                        // Take the last arity arguments.

                        let mut write_terms = stack.terms.write();

                        let length = write_terms.len();

                        let arguments = &write_terms[length - arity..];

                        let term: DataExpression = if arguments.is_empty() {

                            symbol.protect().into()

                            DataApplication::new(tp, &symbol, arguments).into()

                        write_terms.drain(length - arity..);

                        drop(write_terms);

                        drop(write_configs);

                        match InnermostRewriter::find_match(tp, stack, builder, stats, automaton, &term) {

                            Some((announcement, annotation)) => {

                                trace!(

                                let mut write_terms = stack.terms.write();

                                let mut write_configs = stack.configs.write();

                                InnermostStack::integrate(

                                    &mut write_configs,

                                    &mut write_terms,

                                    &annotation.rhs_stack,

                                    &term,

                                    index,

                                );

                                stats.rewrite_steps += 1;

                            None => {

                                // Add the term on the stack.

                                let mut write_terms = stack.terms.write();

                                let t = write_terms.protect(&term);

                                write_terms[index] = t.into();

                            }

                        let mut write_terms = stack.terms.write();

                        return write_terms

                            .pop()

                            .expect("The result should be the last element on the stack")

                            .protect();

                let read_configs = stack.configs.read();

                for (index, term) in stack.terms.read().iter().enumerate() {

                    if term.is_default() {

                        debug_assert!(

                            read_configs.iter().any(|x| {

                                match x {

                                    Config::Return() => true,

                            }),

                    }

    }

    fn find_match<'a>(

        tp: &mut TermPool,

        stack: &mut InnermostStack,

        builder: &mut SCCTBuilder,

        stats: &mut RewritingStatistics,

        automaton: &'a SetAutomaton<AnnouncementInnermost>,

        t: &ATermRef<'_>,

    ) -> Option<(&'a MatchAnnouncement, &'a AnnouncementInnermost)> {

        // Start at the initial state

        let mut state_index = 0;

            let state = &automaton.states[state_index];

            // Get the symbol at the position state.label

            stats.symbol_comparisons += 1;

            let pos: DataExpressionRef<'_> = t.get_position(&state.label).into();

            let symbol = pos.data_function_symbol();

            if let Some(transition) = automaton.transitions.get(&(state_index, symbol.operation_id())) {

                for (announcement, annotation) in &transition.announcements {

                    if check_equivalence_classes(t, &annotation.equivalence_classes)

                        && InnermostRewriter::check_conditions(tp, stack, builder, stats, automaton, annotation, t)

                        return Some((announcement, annotation));

                    }

                if transition.destinations.is_empty() {

                    return None;

                } else {

                    // Continue matching in the next state

                    state_index = transition.destinations.first().unwrap().1;

                }

                return None;

    }

    fn check_conditions(

        tp: &mut TermPool,

        stack: &mut InnermostStack,

        builder: &mut SCCTBuilder,

        stats: &mut RewritingStatistics,

        automaton: &SetAutomaton<AnnouncementInnermost>,

        announcement: &AnnouncementInnermost,

        t: &ATermRef<'_>,

    ) -> bool {

        for c in &announcement.conditions {

            let rhs: DataExpression = c.semi_compressed_rhs.evaluate_with(builder, t, tp).into();

            let lhs: DataExpression = c.semi_compressed_lhs.evaluate_with(builder, t, tp).into();

            let rhs_normal = InnermostRewriter::rewrite_aux(tp, stack, builder, stats, automaton, rhs);

            let lhs_normal = if &lhs == tp.true_term() {

                InnermostRewriter::rewrite_aux(tp, stack, builder, stats, automaton, lhs)

            if lhs_normal != rhs_normal && c.equality || lhs_normal == rhs_normal && !c.equality {

                return false;

            }

        true

    }

    fn new(rule: &Rule) -> AnnouncementInnermost {

        AnnouncementInnermost {

            conditions: extend_conditions(rule),

            equivalence_classes: derive_equivalence_classes(rule),

            rhs_stack: RHSStack::new(rule),

        }

    }

    #[test]