fix bugs in the smt cannonicalazion passes for sdiv and srem

[dominicmkennedy]

There are few bugs in SRemFold and SDivFold.
When the canonicalizer sees constants as operands for the SRem and SDiv operations, it tries to elide the instruction and instead just return the new constant itself, unfortunatly on the edge cases it doesn't actually match z3's semantics.

For SRem when the rhs is 0 then the result should always be the lhs.
For SDiv when there's an underflow it should return INT_MIN, and when there's a div by zero the result should either be one or neg one, depending on sign of lhs

I also took the liberty of adding passes for Udiv and URem.
Not sure if there are unit tests for this part of the codebase, but if so I'd like to add some if I could, just to be extra sure of everything

[math-fehr]

Thanks a lot!
I need to add the proper tests for constant folding, I have some idea that will require to essentially test all possible values with 4 bits, that should do it I think!
Otherwise, the tests are currently just input/output tests in tests/filecheck/canonicalize-smt/ Can you add one simple test just to be sure that this gets called?

[math-fehr]

Suggested change

	if rhs == 0 and isinstance(op.lhs, OpResult):
	rewriter.replace_matched_op(op.lhs.op.clone())
	return
	if rhs == 0:
	rewriter.replace_matched_op([], op.lhs)
	return

[math-fehr]

Suggested change

	if rhs == 0 and isinstance(op.lhs, OpResult):
	rewriter.replace_matched_op(op.lhs.op.clone())
	return
	if rhs == 0:
	rewriter.replace_matched_op([], [op.lhs])
	return