在Z3 中的复数中， Leonardo de Moura 能够在 Z3 中引入和计算复数。
使用 Leonardo 提出的代码，我根据此处提供的代码在 Z3 中引入和计算四元数。使用这个“四元数”代码我正在解决以下问题：
x = Quaternion("x")
s = Tactic('qfnra-nlsat').solver()
s.add(x*x + 30 == 0, x.i3 > 0, x.i2 >0, x.i1 > 0)
print(s.check())
m = s.model()
print m
相应的输出是：
sat
[x.r = 0, x.i1 = 1, x.i2 = 1, x.i3 = 5.2915026221?]
使用 Maple 验证了该结果。
其他示例：
x = Quaternion("x")
y = Quaternion("y")
z = Quaternion("z")
s = Tactic('qfnra-nlsat').solver()
s.add(x*y + 30 + x + y*z == 0, x - y + z == 10)
print(s.check())
m = s.model()
print m
输出是：
sat
[y.r = 1/8,
z.r = 2601/64,
y.i1 = 1/2,
z.i1 = 45/8,
y.i2 = -1/2,
z.i2 = -45/8,
y.i3 = -1/2,
z.i3 = -45/8,
x.i3 = 41/8,
x.i2 = 41/8,
x.i1 = -41/8,
x.r = -1953/64]
其他示例：
证明
x * y != y * x
代码：
x = Quaternion("x")
y = Quaternion("y")
a1, b1, c1, d1 = Reals('a1 b1 c1 d1')
a2, b2, c2, d2 = Reals('a2 b2 c2 d2')
x.r = a1
x.i1 = b1
x.i2 = c1
x.i3 = d1
y.r = a2
y.i1 = b2
y.i2 = c2
y.i3 = d2
print simplify((x * y - y * x).r)
print simplify((x * y - y * x).i1)
print simplify((x * y - y * x).i2)
print simplify((x * y - y * x).i3)
输出：
0
2·c2·d1 + -2·c1·d2
-2·b2·d1 + 2·b1·d2
2·b2·c1 + -2·b1·c2
其他例子：证明四元数
A = (1+ I)/sqrt(2),
B =(1 + J)/sqrt(2),
C = (1 + K)/sqrt(2)
生成编织组的表示，也就是说，我们有
ABA = BAB, ACA = CAC, BCB = CBC.
代码：
A = Quaternion('A')
B = Quaternion('B')
C = Quaternion('C')
A.r = 1/Sqrt(2)
A.i1 = 1/Sqrt(2)
A.i2 = 0
A.i3 = 0
B.r = 1/Sqrt(2)
B.i1 = 0
B.i2 = 1/Sqrt(2)
B.i3 = 0
C.r = 1/Sqrt(2)
C.i1 = 0
C.i2 = 0
C.i3 = 1/Sqrt(2)
print simplify((A*B*A-B*A*B).r)
print simplify((A*B*A-B*A*B).i1)
print simplify((A*B*A-B*A*B).i2)
print simplify((A*B*A-B*A*B).i3)
print "Proved : ABA = BAB:"
print simplify((A*C*A-C*A*C).r)
print simplify((A*C*A-C*A*C).i1)
print simplify((A*C*A-C*A*C).i2)
print simplify((A*C*A-C*A*C).i3)
print "Proved : ACA = CAC:"
print simplify((B*C*B-C*B*C).r)
print simplify((B*C*B-C*B*C).i1)
print simplify((B*C*B-C*B*C).i2)
print simplify((B*C*B-C*B*C).i3)
print "Proved : BCB = CBC:"
输出：
0
0
0
0
Proved : ABA = BAB.
0
0
0
0
Proved : ACA = CAC.
0
0
0
0
Proved : BCB = CBC.
其他例子：证明
x / x = 1
对于所有可逆四元数：
代码：
x = Quaternion("x")
a, a1, a2, a3 = Reals('a a1 a2 a3')
x.r = a
x.i1 = a1
x.i2 = a2
x.i3 = a3
s = Solver()
s.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).r == 1))
print s.check()
s1 = Solver()
s1.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i1 == 0))
print s1.check()
s2 = Solver()
s2.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i2 == 0))
print s2.check()
s3 = Solver()
s3.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i3 == 0))
print s3.check()
输出：
unsat
unsat
unsat
unsat
请让我知道您对“四元数”代码的看法以及如何改进“四元数”代码。非常感谢。