dunderscore operators not defined in base class

[leonardt]

Right now the dunderscore operators (e.g. add) are not defined in the ABC, instead they are defined as bvadd, etc.., then the concrete classes implement them but also have to define the dunderscore methods (e.g. https://github.com/leonardt/hwtypes/blob/master/hwtypes/z3_bit_vector.py#L471-L491 and

hwtypes/hwtypes/bit_vector.py

Lines 341 to 473 in a184707

	def __invert__(self): return self.bvnot()
	def __and__(self, other):
	try:
	return self.bvand(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __or__(self, other):
	try:
	return self.bvor(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __xor__(self, other):
	try:
	return self.bvxor(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __lshift__(self, other):
	try:
	return self.bvshl(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __rshift__(self, other):
	try:
	return self.bvlshr(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __neg__(self): return self.bvneg()
	def __add__(self, other):
	try:
	return self.bvadd(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __sub__(self, other):
	try:
	return self.bvsub(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __mul__(self, other):
	try:
	return self.bvmul(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __floordiv__(self, other):
	try:
	return self.bvudiv(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __mod__(self, other):
	try:
	return self.bvurem(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __eq__(self, other):
	try:
	return self.bveq(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __ne__(self, other):
	try:
	return self.bvne(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __ge__(self, other):
	try:
	return self.bvuge(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __gt__(self, other):
	try:
	return self.bvugt(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __le__(self, other):
	try:
	return self.bvule(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented
	def __lt__(self, other):
	try:
	return self.bvult(other)
	except InconsistentSizeError as e:
	raise e from None
	except TypeError:
	return NotImplemented

)

It seems that we could have these defined in the abstract base class to refer to the abstract methods. The reason it seems for them not being there is that the BV class has a different implementation than the z3 class (special handling for an exception case). Should we instead just have the BV class override the dunderscore methods but have a default version that dispatches to bv<name> methods? Basically, asking if we can have https://github.com/leonardt/hwtypes/blob/master/hwtypes/z3_bit_vector.py#L471-L491 be the default implementation inherited from the ABC.

[leonardt]

I think I see the issue now, basically, we want to return notimplemented in the case that an error occurs to try and dispatch to "other"'s implementation to see if it can handle the inconsistent size. To do this, we need to define the operators in the context of the concrete implementation.

[phanrahan]

When I first implemented the BitVector class, I added bv* methods that were intended to exactly reproduce the SMTBitVector semantics.

[cdonovick]

@leonardt We can add the dunder methods to the base classes. The way things are set up in bitvector is not totally by design.

To get the AssembledADT to work I needed bitvector to return NotImplemented. I couldn't just change my coerce function because it used in a bunch of places. Further I didn't want the bvmethods to return NotImplemented.

In any event I think this will be addressed by the next family construction, although we will need to agree on a set of operators for AbstractBitVector.