pica_mul.py

from z3 import *

def OldMultiply(x, y):
    firstNotNan = And(x == 0.0, Not(fpIsNaN(y)))
    secondNotNan = And(y == 0.0, Not(fpIsNaN(x)))
    shouldZero = Or(firstNotNan, secondNotNan)
    return simplify(If(shouldZero, +0.0, fpMul(RNE(), x, y)))

def NewMultiply(x, y):
    result = fpMul(RNE(), x, y)
    isNan = And(Not(fpIsNaN(x)), Not(fpIsNaN(y)), fpIsNaN(result))
    return simplify(If(isNan, +0.0, result))


x = FP('x', Float32())
y = FP('y', Float32())
s = Solver()
left_hand = OldMultiply(x, y)
right_hand = NewMultiply(x, y)
# Account for the fact that the PICA200 doesn't seem to have a negative 0
s.add(left_hand != FPVal(-0.0, Float32()))
s.add(right_hand != FPVal(-0.0, Float32()))
s.add(x != FPVal(-0.0, Float32()))
s.add(y != FPVal(-0.0, Float32()))
s.add(left_hand != right_hand)

# Individual tests
w = OldMultiply(FPVal(-0.0, Float32()), FPVal(float('+inf'), Float32()))
z = NewMultiply(FPVal(-0.0, Float32()), FPVal(float('+inf'), Float32()))
print("Previous result: {}".format(w))
print("New result: {0}".format(z))

# Check result
if s.check() == sat:
    print("sat: ")
    print(s.model())
else:
    print("unsat")