Improve Workflow and Error Messages

[dz333]

Currently, typechecking SIRRTL requires an external call to the Z3 SMT solver, which is not executed by the compiler. Furthermore, relating SMT failures to IFC errors in the original circuit is nontrivial, especially for implicit flows.

This issue tracks the following:

• Integrate SMT checking into the compiler directly (but still by using an external dependency, such as Z3)
• Integrate support for multiple SMT backends (maybe not necessary due to the dominance of Z3 in practice)
• Improve error reporting given Z3 satisfiability counterexamples.