Refactor out code to get the inits, trs, safes, and axioms from a module

[Alex-Fischman]

Currently, there are at least five different places in the code where this is done (all three bounded model checkers, verify/module.rs, and inference/basics.rs), and they're all done slightly differently. There should be a single function on Modules that can be called to get this information.

Additionally, this function can be smarter than the current implementations are, by (for example) recursing into Ands.

[wilcoxjay]

Thanks for filing this issue! Just to make things a little more concrete, here are the places where we are doing this:

• set checker
• sat checker
• bdd checker
• verify/safety.rs via verify/module.rs
• inference/basics.rs

My impression from glancing through these is that they are all pretty similar. I think the best use of flyvy internal data structures is in verify/safety.rs, so perhaps that is the one to keep. Right now that implementation is somewhat specific to invariant verification, and so would need to be generalized slightly. (Mostly just separating out the conversion to a transition system from the invariant stuff.)

[wilcoxjay]

I propose that we introduce a struct for "first order transition systems" that is similar to verify::safety::InvariantAssertion (but without the invariant stuff) and to inference::basics::FOModule (but without the weird algorithm-specific boolean configuration fields). And we have a new method for this struct that takes a flyvy Module.

[Alex-Fischman]

I'm currently working on this on branch transition-system-extraction.