z3 - 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=-4and满足b=2 所以这意味着 Z3 中的减法是通过从左到右应用二元运算来定义的？

标签： z3smtassociativity

Answer 1

这实际上是 SMT-Lib 的一个特性，z3 只是在实现它。见这里：http ://smtlib.cs.uiowa.edu/theories-Ints.shtml

是的，如果你有多个元素，它只是关联到左边。那是：

 (- 1 2 3 4)

与以下内容完全相同：

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

这确实令人困惑，因为我们只想对括号无关紧要的关联运算符（如+and *）做，但 SMTLib 在这个意义上是自由的。这并不意味着减法在 SMT-Lib 中是关联的，它只是意味着如果您有多个参数，它会按上述方式进行解析。希望有帮助！