計算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)