3 ms·
If you're not a fan of lispy languages, Z3 has bindings for .NET, C, C++, Java, OCaml and Python. For example, Python version of the “x + +0 = x” check looks l
by jwilk 9y ago
If you're not a fan of lispy languages, Z3 has bindings for .NET, C, C++, Java, OCaml and Python.
For example, Python version of the “x + +0 = x” check looks like this:
from z3 import *
s = SolverFor('QF_FP')
x = FP('x', FPSort(11, 53))
z = fpPlusZero(FPSort(11, 53))
r = RNE()
s.add(Not(fpAdd(r, x, z) == x))
print(s.check())
print(s.model())
(Except that I hardcoded rounding-mode, because I couldn't figure out how to make an unknown one. :-/)