Z3中的多元素减法

Question

我正在使用Z3解决需要减法的问题，并且我遇到了这样一个事实，即Z3中的减法允许多个参数。对我来说，这很奇怪，因为减法不是联合运算。这可以从以下脚本中看到。

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (= a (- 1 2 3)))
(assert (= b (- 1 (- 2 3))))
(assert (= c (- (- 1 2) 3)))

[a=c=-4和b=2满足因此，这意味着Z3中的减法是通过从左到右应用二进制运算来定义的？

Answer 1

这实际上是SMT-Lib的功能，z3只是实现了这一功能。看到这里：http://smtlib.cs.uiowa.edu/theories-Ints.shtml

[是的，如果您有多个元素，它只会与左侧关联。那是：

 (- 1 2 3 4)

与以下内容完全相同：

 (- (- (- 1 2) 3) 4)

这确实令人困惑，因为我们只想对括号无关紧要的关联运算符（例如+和*）进行操作，但是SMTLib在这种意义上是自由的。这确实意味着减法在SMT-Lib中是关联的，仅表示如果您有多个参数，则如上所述将其解析。希望能有所帮助！