[SMT] Add quantifier attribute and pattern support to ExportSMTLIB

[maerhart]

The SMT operations smt.forall and smt.exists support attributes called weight and no_pattern to give hints to the solver backend (e.g., Z3). We should add support for them in the ExportSMTLIB pass. Currently, it just errors out when it encounters those attributes:

https://github.com/llvm/circt/blob/6d4939d89d55d0c3ef4001fe8afafa24997d3e9d/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp#L295-L301

Furthermore, the quantifier operations allow a variadic number of regions representing a multi-pattern each, i.e., each region should be emitted as one :pattern attribute such that each operand of the smt.yield operation in the region represents one pattern in the multi-pattern.

Information on how such attributes have to be annotated in SMT-LIB can be found in the SMT-LIB standard version 2.6 sections 3.6.5 and 3.6.6

Z3-specific documentation of those features can be found here: https://microsoft.github.io/z3guide/docs/logic/Quantifiers/#patterns https://microsoft.github.io/z3guide/docs/logic/Quantifiers/#multi-patterns https://microsoft.github.io/z3guide/docs/logic/Quantifiers/#no-patterns

[luisacicolini]

Happy to work on this!