Search code examples
z3z3py

Taking the floor of a real number in Z3Py

Given a real number like Real('x') in Z3Py, how do I get its floor or ceiling? Equivalently, how do I round it? I see that to_int is a thing in the SMT specification, but I don't know how to call it from Python.

Solution

  • The function "ToInt" takes the floor.

    from z3 import *

x = Real('x')
print ToInt(x)
print ToInt(RealVal("1/2"))
print simplify(ToInt(RealVal("1/2")))