pub fn new(pattern: DataExpression, position: DataPosition) -> Self {

        MatchObligation { pattern, position }

    }

    pub fn new<F>(spec: &RewriteSpecification, annotate: F, apma: bool) -> SetAutomaton<M>

    where

        F: Fn(&Rule) -> M,

        let start = Instant::now();

        let mut state_counter: usize = 1;

        let supported_rules: Vec<Rule> = spec

            .rewrite_rules()

            .iter()

            .filter(|rule| is_supported_rule(rule))

            .map(Rule::clone)

            .collect();

        let symbols = {

            let mut symbols = HashMap::default();

            for rule in &supported_rules {

                find_symbols(&rule.lhs.copy(), &mut symbols);

                find_symbols(&rule.rhs.copy(), &mut symbols);

                for cond in &rule.conditions {

                    find_symbols(&cond.lhs.copy(), &mut symbols);

                    find_symbols(&cond.rhs.copy(), &mut symbols);

                }

            symbols

        for (index, (symbol, arity)) in symbols.iter().enumerate() {

            trace!("{index}: {symbol} {arity}");

        let mut initial_match_goals = Vec::<MatchGoal>::new();

        for rr in &supported_rules {

            initial_match_goals.push(MatchGoal::new(

                MatchAnnouncement {

                    rule: (*rr).clone(),

                    position: DataPosition::empty(),

                    symbols_seen: 0,

                },

                vec![MatchObligation::new(rr.lhs.clone(), DataPosition::empty())],

            ));

        }

        initial_match_goals.sort();

        let initial_state = State {

            label: DataPosition::empty(),

            match_goals: initial_match_goals.clone(),

        };

        let mut map_goals_state = HashMap::default();

        let mut queue = VecDeque::new();

        queue.push_back(0);

        map_goals_state.insert(initial_match_goals, 0);

        let mut states = vec![initial_state];

        let mut transitions = FxHashMap::default();

        while let Some(s_index) = queue.pop_front() {

            for (symbol, arity) in &symbols {

                let (mut announcements, pos_to_goals) =

                    states

                        .get(s_index)

                        .unwrap()

                        .derive_transition(symbol, *arity, &supported_rules, apma);

                announcements.sort_by(|ma1, ma2| ma1.position.cmp(&ma2.position));

                let mut destinations = smallvec![];

                for (pos, goals_or_initial) in pos_to_goals {

                    if let GoalsOrInitial::Goals(goals) = goals_or_initial {

                        if map_goals_state.contains_key(&goals) {

                            destinations.push((pos, *map_goals_state.get(&goals).unwrap()))

                        } else if !goals.is_empty() {

                            // The destination state does not yet exist, create it

                            let new_state = State::new(goals.clone());

                            states.push(new_state);

                            destinations.push((pos, state_counter));

                            map_goals_state.insert(goals, state_counter);

                            queue.push_back(state_counter);

                            state_counter += 1;

                        }

                    } else {

                        // The transition is to the initial state

                        destinations.push((pos, 0));

                    }

                let announcements = announcements

                    .into_iter()

                    .map(|ma| {

                        let annotation = annotate(&ma.rule);

                        (ma, annotation)

                    })

                    .collect();

                debug_assert!(

                    !&transitions.contains_key(&(s_index, symbol.operation_id())),

                transitions.insert(

                    (s_index, symbol.operation_id()),

                    Transition {

                        symbol: symbol.clone(),

                        announcements,

                        destinations,

                    },

            debug!(

        if !log_enabled!(log::Level::Debug) {

            for state in &mut states {

                state.match_goals.clear();

            }

        info!(

            states.len(),

            transitions.len(),

            (Instant::now() - start).as_millis()

        let result = SetAutomaton { states, transitions };

        debug!("{result:?}");

        result

    }

    pub fn states(&self) -> &[State] {

        &self.states

    }

    pub fn get_transition(&self, state: usize, operation_id: usize) -> Option<&Transition<M>> {

        self.transitions.get(&(state, operation_id))

    }

    pub fn iter_transitions(&self) -> impl Iterator<Item = (usize, usize, &Transition<M>)> {

        self.transitions

            .iter()

            .map(|(&(state, operation_id), transition)| (state, operation_id, transition))

    }

    fn derive_transition(

        &self,

        symbol: &DataFunctionSymbol,

        arity: usize,

        rewrite_rules: &[Rule],

        apma: bool,

    ) -> (Vec<MatchAnnouncement>, Vec<(DataPosition, GoalsOrInitial)>) {

        let mut derivative = self.compute_derivative(symbol, arity);

        let outputs = derivative.completed.into_iter().map(|x| x.announcement).collect();

        let mut new_match_goals = derivative.unchanged;

        new_match_goals.append(&mut derivative.reduced);

        let mut destinations = vec![];

        if apma {

            if !new_match_goals.is_empty() {

                destinations.push((DataPosition::empty(), GoalsOrInitial::Goals(new_match_goals)));

            }

            let partitioned = MatchGoal::partition(new_match_goals);

            let mut positions_per_partition = vec![];

            let mut gcp_length_per_partition = vec![];

            for (p, pos) in partitioned {

                positions_per_partition.push(pos);

                let gcp = MatchGoal::greatest_common_prefix(&p);

                let gcp_length = gcp.len();

                gcp_length_per_partition.push(gcp_length);

                let mut goals = MatchGoal::remove_prefix(p, gcp_length);

                goals.sort_unstable();

                destinations.push((gcp, GoalsOrInitial::Goals(goals)));

            }

            for i in 1..arity + 1 {

                let mut pos = self.label.clone();

                pos.push(i);

                let mut partition_key = None;

                'outer: for (i, part_pos) in positions_per_partition.iter().enumerate() {

                    for p in part_pos {

                        if MatchGoal::pos_comparable(p, &pos) {

                            partition_key = Some(i);

                            break 'outer;

                        }

                if let Some(key) = partition_key {

                    let gcp_length = gcp_length_per_partition[key];

                    let pos = DataPosition::new(&pos.indices()[gcp_length..]);

                    for rr in rewrite_rules {

                        if let GoalsOrInitial::Goals(goals) = &mut destinations[key].1 {

                            goals.push(MatchGoal {

                                obligations: vec![MatchObligation::new(rr.lhs.clone(), pos.clone())],

                                announcement: MatchAnnouncement {

                                    rule: (*rr).clone(),

                                    position: pos.clone(),

                                    symbols_seen: 0,

                                },

                            });

                        }

                } else {

                    // The transition is simply to the initial state

                    // GoalsOrInitial::InitialState avoids unnecessary work of creating all these fresh goals

                    destinations.push((pos, GoalsOrInitial::InitialState));

                }

        destinations.sort_unstable_by(|(pos1, _), (pos2, _)| pos1.cmp(pos2));

        (outputs, destinations)

    }

    fn compute_derivative(&self, symbol: &DataFunctionSymbol, arity: usize) -> Derivative {

        let mut result = Derivative {

            completed: vec![],

            unchanged: vec![],

            reduced: vec![],

        };

        for mg in &self.match_goals {

            debug_assert!(

                !mg.obligations.is_empty(),

            if mg.obligations.len() == 1

                && mg.obligations.iter().any(|mo| {

                    mo.position == self.label

                        && mo.pattern.data_function_symbol() == symbol.copy()

                        && mo.pattern.data_arguments().all(|x| is_data_variable(&x))

                })

            {

                result.completed.push(mg.clone());

            } else if mg

                .obligations

                .iter()

                .any(|mo| mo.position == self.label && mo.pattern.data_function_symbol() != symbol.copy())

            {

                // Match goal is discarded since head symbol does not match.

            } else if mg.obligations.iter().all(|mo| mo.position != self.label) {

                let mut mg = mg.clone();

                if mg.announcement.rule.lhs != mg.obligations.first().unwrap().pattern {

                    mg.announcement.symbols_seen += 1;

                }

                result.unchanged.push(mg.clone());

                let mut mg = mg.clone();

                let mut new_obligations = vec![];

                for mo in mg.obligations {

                    if mo.pattern.data_function_symbol() == symbol.copy() && mo.position == self.label {

                        for (index, t) in mo.pattern.data_arguments().enumerate() {

                            assert!(

                                index < arity,

                            if !is_data_variable(&t) {

                                let mut new_pos = mo.position.clone();

                                new_pos.push(index + 1);

                                new_obligations.push(MatchObligation {

                                    pattern: t.protect(),

                                    position: new_pos,

                                });

                            }

                    } else {

                        // remains unchanged

                        new_obligations.push(mo.clone());

                    }

                new_obligations.sort_unstable_by_key(|mo1| mo1.position.len());

                mg.obligations = new_obligations;

                mg.announcement.symbols_seen += 1;

                result.reduced.push(mg);

        trace!(

        trace!("Match goals: {{");

        for mg in &self.match_goals {

            trace!("\t {mg:?}");

        trace!("}}");

        trace!("Completed: {{");

        for mg in &result.completed {

            trace!("\t {mg:?}");

        trace!("}}");

        trace!("Unchanged: {{");

        for mg in &result.unchanged {

            trace!("\t {mg:?}");

        trace!("}}");

        trace!("Reduced: {{");

        for mg in &result.reduced {

            trace!("\t {mg:?}");

        trace!("}}");

        result

    }

    fn new(goals: Vec<MatchGoal>) -> State {

        let mut label: Option<DataPosition> = None;

        for goal in &goals {

            if goal.announcement.position.is_empty() {

                if label.is_none() {

                    label = Some(goal.obligations.first().unwrap().position.clone());

                }

                for obligation in &goal.obligations {

                    if let Some(l) = &label

                        && &obligation.position < l

                    {

                        label = Some(obligation.position.clone());

                    }

            }

        State {

            label: label.unwrap(),

            match_goals: goals,

        }

    }

    pub fn label(&self) -> &DataPosition {

        &self.label

    }

    pub fn match_goals(&self) -> &[MatchGoal] {

        &self.match_goals

    }

fn add_symbol(function_symbol: DataFunctionSymbol, arity: usize, symbols: &mut HashMap<DataFunctionSymbol, usize>) {

    if let Some(x) = symbols.get(&function_symbol) {

        assert_eq!(

    } else {

        symbols.insert(function_symbol, arity);

    }

}

fn is_supported_term(t: &DataExpression) -> bool {

    for subterm in t.iter() {

        if is_data_application(&subterm) && !is_data_function_symbol(&subterm.arg(0)) {

        }

    true

}

pub fn is_supported_rule(rule: &Rule) -> bool {

    if !is_supported_term(&rule.rhs) || !is_supported_term(&rule.lhs) {

    }

    for cond in &rule.conditions {

        if !is_supported_term(&cond.rhs) || !is_supported_term(&cond.lhs) {

        }

    true

}

fn find_symbols(t: &DataExpressionRef<'_>, symbols: &mut HashMap<DataFunctionSymbol, usize>) {

    if is_data_function_symbol(t) {

        add_symbol(t.protect().into(), 0, symbols);

    } else if is_data_application(t) {

        assert!(

            is_data_function_symbol(&t.data_function_symbol()),

        add_symbol(t.data_function_symbol().protect(), t.data_arguments().len(), symbols);

        for arg in t.data_arguments() {

            find_symbols(&arg, symbols);

        }

    } else if is_data_machine_number(t) {

    } else if !is_data_variable(t) {

    }

}