我如何在Z3-PY中实现C位运算符？

from z3 import *

# 定义两个二进制数的变量
a = BitVec('a', 32)
b = BitVec('b', 32)

# 定义C位运算符的函数
def c_and(x, y):
    return (x & y) == (x | y)

def c_or(x, y):
    return (x | y) == (x & y)

def c_xor(x, y):
    return (x ^ y) == (x & y)

# 创建Z3求解器
solver = Solver()

# 添加约束条件
solver.add(c_and(a, b))

# 求解并输出结果
if solver.check() == sat:
    model = solver.model()
    print("满足C位运算符的解为：")
    print("a =", model[a])
    print("b =", model[b])
else:
    print("无解")