计算Z3中的绝对值

Question

我有3个变量a,b和c。我需要计算c = 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)))) 

下面是完整的例子（也可用online at 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)