Chore: Add Documentation to Automata Tactic

[AtticusKuhn]

Add documentation explaining the purpose and inner workings of the automata tactic.

CC: @Superty because he was asking about how the automata tactic functions.

[github-actions[bot]]

Alive Statistics: 64 / 93 (29 failed)

[bollu]

I don’t have the rest of the context here, but to handle negations, we use the fact that regular expressions are closed under complementation.

On Fri, Aug 9, 2024, at 11:52, Arjun P wrote:

@.**** commented on this pull request.

In SSA/Experimental/Bits/Fast/README.md https://github.com/opencompl/lean-mlir/pull/526#discussion_r1711801085:

+The reason that this tactic only accepts operations of constant memory is that this corresponds to state machines with a finite number of states. +If we accepted multiplication as an operation, the number of states in the state machine could potentially blow up. + +# How is the Automata Tactic Implemented? + +To figure out if + +[a = b] + +we ask: +Does the automaton + +[automaton(a ^^^ b)] + +accept the string of all zeros?

this seems to contradict with the definition below involving arities > 0. I would guess that the thing is nondeterministic over the free variable transitions, forming an NFA, and then we ask if there is any non-deterministic path where the NFA rejects. (opposite to the usual notion of NFAs, where they accept iff there is some path to the accept state, here we are actually asking whether there is any path to the reject state.) I'm guessing you then convert the NFA to a DFA and you have to check whether the resulting DFA accepts iff the input is all zeros of some length.

— Reply to this email directly, view it on GitHub https://github.com/opencompl/lean-mlir/pull/526#pullrequestreview-2230656695, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAM5ZDM4HJL2VG22XDNKECDZQTXVJAVCNFSM6AAAAABMIV456SVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMZDEMZQGY2TMNRZGU. You are receiving this because you are subscribed to this thread.Message ID: @.***>

http://pixel-druid.com/

[Superty]

yeah you can just swap the accept and reject states -- just didn't want to cause confusion because in the examples in the document, the Accept and Reject states are opposite from what I expect you need in the NFA.

[tobiasgrosser]

@AtticusKuhn, are you planning to update this PR. It might be useful to get it merged such that it does not get out-of-date.

[AtticusKuhn]

@AtticusKuhn, are you planning to update this PR. It might be useful to get it merged such that it does not get out-of-date.

Well, as I wrote this PR, I realised that I understood less of the internals of how the automata tactic works than I originally thought.