Lazy evaluation of operations to get some accepted word

[jurajsic]

For Z3-Noodler, I need to get a word from application of operations on automata while not constructing the resulting automaton (as it can blow-up). More specifically I need:

• [ ] a word from a complement of an NFA, without computing the whole complement
• [ ] having two NFAs A1 and A2, I need a word from L(A1) ∩ L(A2)', where again, the complement is the problem

The first problem could be solved by doing determinization and stopping when some macrostate does not contain any final state. The second is harder, I do not know how to do it.

[vhavlena]

The second one is language difference, no? It should be similar to the first case, the only difference is that a macrostate looks like (q,S) not just S.

[jurajsic]

Yes, it's language difference. And yes, the macrostate would be (q,S), but I think implementation-wise it will be harder (for the first case, we can just reuse the determinization implementation).

[Adda0]

For the implementation of get_word_from_complement(Nfa nfa_to_complement), we could modify the existing determinization algorithm. We could add an optional callback function, similarly to how we handle callback functions in Tarjan's algorithm, for example, where the callback would be an event handler for encountering a new macrostate. If the callback is defined and returns true, the determinization continues, otherwise the determinization stops. In this case, the callback would check the final states in the macrostate and return false if there is none (the macrostate is a final state in the complement). The determinization then returns the DFA created so far.

For the language difference, this callback could be maybe utilized, too. However, you would have to take into account the transition symbols leading to this macrostate. Or possibly the outgoing transition symbols.

Does this sound reasonable?

[vhavlena]

It could work. It is quite useful to add the language difference operation and then this kind of callback extension should be easy.

[Adda0]

I have implemented nfa::Nfa::get_word_from_complement(). The PR will be created once the PRs the implementation depends on get merged.