[Z3] Add missing division operations in BitVector

src/Z3-Tests/BVTest.class.st

@@ -78,6 +78,26 @@ BVTest >> testCoerceBitAnd [
 	self assert: x & 16rF0 equals: 2r10100000
 ]
 
+{ #category : #bv }
+BVTest >> testCoerceSignedModulo [
+	"9 \\ -4 >>> -3"
+	| nine |
+	nine := 9 toBitVector: 32.
+	self
+		assert: (nine \\ -4) signedValue
+		equals: -3
+]
+
+{ #category : #bv }
+BVTest >> testCoerceSignedRemainder [
+	"9 \\ -4 >>> -3"
+	| nine |
+	nine := 9 toBitVector: 32.
+	self
+		assert: (nine srem: -4) signedValue
+		equals: 1
+]
+
 { #category : #rewriting }
 BVTest >> testThisEnvironment [
 	self doTestThisEnvironment: 2r1111

src/Z3/BitVector.class.st

@@ -158,6 +158,17 @@ BitVector >> >> shamt [
 	^ self bitShiftRight: shamt
 ]
 
+{ #category : #arithmetic }
+BitVector >> \\ rhs [
+	"Two's complement signed remainder (sign follows divisor)"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvsmod: ctx _: self _: rhs.
+	].
+	^self retry: #\\ coercing: rhs
+
+]
+
 { #category : #comparing }
 BitVector >> between: min and: max [
 	^self >= min & (self <= max)
@@ -355,6 +366,17 @@ BitVector >> signedValue [
 
 ]
 
+{ #category : #arithmetic }
+BitVector >> srem: rhs [
+	"Two's complement signed remainder (sign follows dividend)"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvsrem: ctx _: self _: rhs.
+	].
+	^self retry: #srem: coercing: rhs
+
+]
+
 { #category : #slicing }
 BitVector >> subrange: anInterval [
 	^(self copyFrom: anInterval first to: anInterval last) simplify
@@ -377,6 +399,17 @@ BitVector >> udiv: rhs [
 
 ]
 
+{ #category : #arithmetic }
+BitVector >> urem: rhs [
+	"Unsigned remainder"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvurem: ctx _: self _: rhs.
+	].
+	^self retry: #urem: coercing: rhs
+
+]
+
 { #category : #'bit operators' }
 BitVector >> | rhs [
 	"Bitwise or"