Z3 不支持这样的矩阵，因此对它们进行编码的最佳方法是对它们表示的公式进行编码。这与数独示例的编码方式大致相同。这是一个简单的示例，例如使用 2x2 实数矩阵（Z3py 链接：http://rise4fun.com/Z3Py/MYnB http://rise4fun.com/Z3Py/MYnB ):
# nonlinear version, constants a_ij, b_i are variables
# x_1, x_2, a_11, a_12, a_21, a_22, b_1, b_2 = Reals('x_1 x_2 a_11 a_12 a_21 a_22 b_1 b_2')
# linear version (all numbers are defined values)
x_1, x_2 = Reals('x_1 x_2')
# A matrix
a_11 = 1
a_12 = 2
a_21 = 3
a_22 = 5
# b-vector
b_1 = 7
b_2 = 11
newx_1 = a_11 * x_1 + a_12 * x_2 + b_1
newx_2 = a_21 * x_1 + a_22 * x_2 + b_2
print newx_1
print newx_2
# solve using model generation
s = Solver()
s.add(newx_1 == 0) # pointers to equations
s.add(newx_2 == 5)
print s.check()
print s.model()
# solve using "solve"
solve(And(newx_1 == 0, newx_2 == 5))
要让 Z3 求解未知矩阵实体，请取消注释第二行（带有 a_11、a_12 等的符号名称），在第五行注释 x_1、x_2 的其他符号定义，并注释对 a_11 的具体赋值= 1 等。然后，您将通过找到对这些变量的满意分配来让 Z3 求解任何未知数，但请注意，您可能需要为您的目的启用模型完成（例如，如果您需要对所有未知矩阵参数进行分配）或 x_i 变量，请参见，例如：Z3 4.0：获取完整模型 https://stackoverflow.com/questions/11115004/z3-4-0-get-complete-model ).
但是，根据您共享的链接，您有兴趣使用正弦曲线（旋转）执行操作，这些操作通常是超越的，而 Z3 目前不支持超越（一般指数等）。这对您来说将是具有挑战性的部分，例如，证明操作有效的任何旋转角度选择，甚至只是对旋转进行编码。缩放和平移不应该太难编码。
另请参阅以下答案，了解如何对线性微分方程进行编码，线性微分方程是 x' = Ax 形式的方程，其中 A 是 n * n 矩阵，x 是 n 维向量：将一阶微分方程编码为一阶公式 https://stackoverflow.com/questions/11927114/encoding-of-first-order-differential-equation-as-first-order-formula/11936271#11936271
