[Z3] Add missing bitwise operations on BitVectors

src/MathNotation/BitVector.extension.st

@@ -0,0 +1,13 @@
+Extension { #name : #BitVector }
+
+{ #category : #'*MathNotation' }
+BitVector >> ⊕ [ rhs
+	"Bitwise exclusive-or.
+	
+	We prefer the selector from Claude Shannon's
+	'Symbolic Analysis of Relay and Switching Circuits' (1938);
+	Boole's ≠ and Church's ≢ don't seem applicable because they
+	take single-bit inputs.	"
+
+	^ self bitXor: rhs
+]

src/Z3-Tests/BVTest.class.st

@@ -71,6 +71,13 @@ BVTest >> testBvEF [
 
 ]
 
+{ #category : #bv }
+BVTest >> testCoerceBitAnd [
+	| x |
+	x := 2r10101010 toBitVector: 8.
+	self assert: x & 16rF0 equals: 2r10100000
+]
+
 { #category : #rewriting }
 BVTest >> testThisEnvironment [
 	self doTestThisEnvironment: 2r1111

src/Z3/BitVector.class.st

@@ -40,6 +40,8 @@ BitVector class >> value: anInteger length: xlen [
 
 { #category : #'bit operators' }
 BitVector >> & rhs [
+	"Bitwise and"
+
 	^ self bitAnd: rhs
 
 ]
@@ -180,6 +182,28 @@ BitVector >> bitInvert [
 
 ]
 
+{ #category : #'bit operators' }
+BitVector >> bitNand: rhs [
+	"Bitwise nand"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvnand: ctx _: self _: rhs.
+	].
+	^self retry: #bitNand: coercing: rhs
+
+
+]
+
+{ #category : #'bit operators' }
+BitVector >> bitNor: rhs [
+	"Bitwise nor"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvor: ctx _: self _: rhs.
+	].
+	^self retry: #bitOr: coercing: rhs
+]
+
 { #category : #'bit operators' }
 BitVector >> bitOr: rhs [
 	"Bitwise or"
@@ -232,6 +256,26 @@ BitVector >> bitShiftRightArithmetic: shamt [
 	^self retry: #bitShiftRightArithmetic: coercing: shamt
 ]
 
+{ #category : #'bit operators' }
+BitVector >> bitXnor: rhs [
+	"Bitwise exclusive-or"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvxnor: ctx _: self _: rhs.
+	].
+	^self retry: #bitXnor: coercing: rhs
+]
+
+{ #category : #'bit operators' }
+BitVector >> bitXor: rhs [
+	"Bitwise exclusive-or"
+
+	(self isLikeMe: rhs) ifTrue:[
+		^ Z3 mk_bvxor: ctx _: self _: rhs.
+	].
+	^self retry: #bitXor: coercing: rhs
+]
+
 { #category : #slicing }
 BitVector >> copyFrom: start to: stop [
 	"This is like the usual SequenceableCollection>>copyFrom:to:,
@@ -268,6 +312,22 @@ BitVector >> printString [
 
 ]
 
+{ #category : #'bit operators' }
+BitVector >> redAnd [
+	"Take conjunction of all bits in the receiver, answer vector of length 1
+	 (1 if all bits of the receiver are ones; 0 if any bit is zero)."
+	^Z3 mk_bvredand: ctx _: self
+
+]
+
+{ #category : #'bit operators' }
+BitVector >> redOr [
+	"Take disjunction of all bits in the receiver, answer vector of length 1
+	 (1 if any bit of the receiver is set to 1, 0 if they are all zeros)."
+	^Z3 mk_bvredor: ctx _: self
+
+]
+
 { #category : #slicing }
 BitVector >> repeat: n [
 	^ Z3 mk_repeat: ctx _: n _: self
@@ -319,6 +379,8 @@ BitVector >> udiv: rhs [
 
 { #category : #'bit operators' }
 BitVector >> | rhs [
+	"Bitwise or"
+
 	^ self bitOr: rhs
 
 ]