\myheading{Proving several floor()/ceiling() properties using Z3}

I've found couple problems in [James L. Hein -- Discrete Structures, Logic, and Computability].
First is:

\begin{lstlisting}
Find numbers x and y such that floor(x + y) != floor(x) + floor(y) and ceiling(x + y) != ceiling(x) + ceiling(y).
\end{lstlisting}

I can emulate real numbers using fixed point arithmetic over bitvectors.
In a 16-bit variable, high 8-bit part will be integer part and low 8-bit part is fractional part.
This is also called Q8.8\footnote{\url{https://en.wikipedia.org/wiki/Fixed-point_arithmetic}}.

floor() function is simple --- just zero fractional part (low 8 bits).
ceiling() function --- if \textit{something} is present in fractional part (low 8 bits), increment high 8 bits.

\begin{lstlisting}[style=custompy]
from z3 import *

# Find numbers x and y such that floor(x + y) != floor(x) + floor(y) and 
# ceiling(x + y) != ceiling(x) + ceiling(y).

def floor(x):
    return x&0xff00

def ceiling(x):
    return If((x&0xff)!=0, (x&0xff00)+0x100, x)

s=Solver()

x,y = BitVecs('x y', 16)

s.add(floor(x+y) != floor(x) + floor(y))
s.add(ceiling(x+y) != ceiling(x) + ceiling(y))

print s.check()
m=s.model()

print "x=0x%04x or %f" % (m[x].as_long(), float(m[x].as_long())/0x100)
print "y=0x%04x or %f" % (m[y].as_long(), float(m[y].as_long())/0x100)
\end{lstlisting}

\begin{lstlisting}[caption=Output]
sat
x=0x03e0 or 3.875000
y=0x3f20 or 63.125000
\end{lstlisting}

Let's check this in Wolfram Mathematica:

\begin{lstlisting}[caption=Output of Wolfram Mathematica]
In[]:= x = 3.875;

In[]:= y = 63.125;

In[]:= {Floor[x + y], Floor[x] + Floor[y]}
Out[]= {67, 66}

In[]:= {Ceiling[x + y], Ceiling[x] + Ceiling[y]}
Out[]= {67, 68}
\end{lstlisting}

The second problem:

\begin{lstlisting}[style=custompy]
from z3 import *

# Find the values of x that satisfy each of the following equations.
# a. ceiling((x - 1)/2) = floor(x/2)
# b. ceiling((x - 1)/3) = floor(x/3)

def floor(x):
    return x&0xff00

def ceiling(x):
    return If((x&0xff)!=0, (x&0xff00)+0x100, x)

s=Solver()

x = BitVec('x', 16)

# 1 in Q8.8 is just 0x0100 or 1<<8
s.add(ceiling((x-0x100)/2) == floor(x/2))
#s.add(ceiling((x-0x100)/3) == floor(x/3))

print s.check()
m=s.model()

print "x=0x%04x or %f" % (m[x].as_long(), float(m[x].as_long())/0x100)
\end{lstlisting}

\begin{lstlisting}[caption=Output for (a)]
sat
x=0x4000 or 64.000000
\end{lstlisting}

\begin{lstlisting}[caption=Output for (b)]
sat
x=0x0000 or 0.000000
\end{lstlisting}

The next problem (unsat for all).

\ac{IFF} is just "==" in Z3, so to find counterexample (if any), we just use "!=".

\begin{lstlisting}[style=custompy]
from z3 import *

"""
Prove each of the following statements about inequalities with the floor and ceiling,
where x is a real number and n is an integer.
a. floor(x) < n iff x < n.
b. n < ceiling(x) iff n < x.
c. n <= floor(x) iff n <= x.
d. floor(x) <= n iff x <= n.
"""

def floor(x):
    return x&0xff00

def ceiling(x):
    return If((x&0xff)!=0, (x&0xff00)+0x100, x)

s=Solver()

x = BitVec('x', 16)
n = BitVec('n', 16)

s.add((n&0xff)==0) # n is always integer, it has no fraction

# prevent integer overflow, x and n must be positive
s.add(x<0x8000)
s.add(n<0x8000)

s.add((floor(x) < n) != (x < n)) # a
#s.add((n < ceiling(x)) != (n < x)) # b
#s.add((n <= floor(x)) != (n <= x)) # c
#s.add((floor(x) <= n) != (x <= n)) # d

# must be unsat for a/b/c/d
print s.check()
\end{lstlisting}

Problem 4, also unsat for all:

\begin{lstlisting}[style=custompy]
from z3 import *

"""
Prove each statement, where n is an integer.
a. ceiling(n/2) = floor((n + 1)/2)
b. floor(n/2) = ceiling((n - 1)/2)
"""

def floor(x):
    return x&0xff00

def ceiling(x):
    return If((x&0xff)!=0, (x&0xff00)+0x100, x)

s=Solver()

n = BitVec('n', 16)

s.add((n&0xff)==0) # n is always integer, it has no fraction

# prevent integer overflow, n is always positive
s.add(n<0x8000)

s.add(ceiling(n/2) != (floor((n+0x100)/2))) # a
#s.add(floor(n/2) != (ceiling((n-0x100)/2))) # b

# must be unsat for a/b
print s.check()
\end{lstlisting}