#!/usr/bin/env python3
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)

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

# 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())