z3 - 计算 Z3 中的绝对值

Question

我有 3 个变量a和. 我需要计算。bcc = absolute(b-a)

我在 Z3 中将此语句编码为

(assert (>= c 0))
(assert (or (= c (- a b) (= c (- b a))))

我在想，有没有更有效的方法在 Z3 中编写它？
Z3内部是否支持计算绝对值？
另外，我希望编写这样的代码不会有任何性能损失，而不是使用其他方式。

Answer 1

您的编码是正确的。然而，用户通常使用编码绝对值函数

(define-fun absolute ((x Int)) Int
  (ite (>= x 0) x (- x)))

然后，他们可以编写约束，例如：

(assert (= c (absolute (- a b))))

这是完整的示例（也可以在rise4fun 在线获得）：

(define-fun absolute ((x Int)) Int
  (ite (>= x 0) x (- x)))

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)

(assert (= a 3))
(assert (= b 4))

(assert (= c (absolute (- a b))))

(check-sat)
(get-model)