[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:

circt/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp

Lines 295 to 301 in 6d4939d

	// TODO: add support
	if (op.getWeight() != 0)
	return op.emitError() << "non-zero weights not supported yet";
	if (op.getNoPattern())
	return op.emitError() << "no-pattern attribute not supported yet";
	if (!op.getPatterns().empty())
	return op.emitError() << "patterns not supported yet";

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!