我想证明涉及矩阵和向量的表达式的属性（可能很大，但大小是固定的）。
例如我想证明一个表达式的结果是对角矩阵或三角矩阵，或者是正定的，...
为此，我想从线性代数中编码众所周知的属性和身份，例如：
||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
det(A+B) = det(A) + det(B)
Tr(zA) = z * Tr(A)
(I + AB) ^ (-1) = I - A(I + BA) ^ (-1) * B
...
我试图在 Z3 中实现这一点。但即使对于简单的属性，它也会返回未知或超时。我尝试过数组理论和量词。
我想知道这个问题是否可以用 SMT 求解器解决，还是不适合这类问题？你能举一个小例子来暗示吗？
Rust书解释了如何使用struct update语法来创建只更新了几个字段的struct的副本.
let mut point = Point3d { x: 0, y: 0, z: 0 };
point = Point3d { y: 1, .. point };
它也不必是相同的结构,可以在创建新结构时使用此语法.
let origin = Point3d { x: 0, y: 0, z: 0 };
let point = Point3d { y: 1, .. origin };
我的问题是关于第二个例子.
如果该origin点永远不会再次使用,编译器是否仍会使(几乎)所有字段的代价变得昂贵(如果字段很大),或者它是否只更新已更新的字段并等同于第一个示例？
如果它就地更新:编译器如何确定它是否可以覆盖origin值？