使用Z3和smtlib以混合值計算配置/模型

Question

如何計算屬性值？ 下面是一個例子：

(declare-fun x() bool) 
(declare-fun y() bool) 
(declare-fun z() bool) 
(assert (AND x (OR y z))) 

有了這個，我會得到2種型號：

x=true and y=true 
x=true and z=true 

現在，我想是這樣的：

(declare-fun x() bool) 
(declare-fun y() bool) 
(declare-fun z() bool) 
(declare-fun x.val() Int) 
(declare-fun y.val() Int) 
(declare-fun z.val() Int) 
(assert (= x.val 2)) 
(assert (= y.val 3)) 
(assert (= z.val 5)) 
(assert (AND x (OR y z))) 
(assert (> sum 6)) 

所以，我想獲得屬性總和大於6的模型：

x=true and z=true 

與陣列也許是工作的方式來實現這一目標？

Answer 1

我不確定是否正確理解您的問題。 看來你想把一個（整數）屬性關聯到每個布爾變量。 所以，每個變量都是一對：一個布爾值和一個整數屬性。 我假設sum，你的意思是分配給true的變量的屬性總和。 如果是這樣的話，你可以用以下方式在Z3中對其進行建模：

;; Enable model construction 
(set-option :produce-models true) 

;; Declare a new type (sort) that is a pair (Bool, Int). 
;; Given a variable x of type/sort WBool, we can write 
;; - (value x) for getting its Boolean value 
;; - (attr x) for getting the integer "attribute" value 
(declare-datatypes() ((WBool (mk-wbool (value Bool) (attr Int))))) 

;; Now, we declare a macro int-value that returns (attr x) if 
;; (value x) is true, and 0 otherwise 
(define-fun int-value ((x WBool)) Int 
    (ite (value x) (attr x) 0)) 

(declare-fun x() WBool) 
(declare-fun y() WBool) 
(declare-fun z() WBool) 

;; Set the attribute values for x, y and z 
(assert (= (attr x) 2)) 
(assert (= (attr y) 3)) 
(assert (= (attr z) 5)) 

;; Assert Boolean constraint on x, y and z. 
(assert (and (value x) (or (value y) (value z)))) 

;; Assert that the sum of the attributes of the variables assigned to true is greater than 6. 
(assert (> (+ (int-value x) (int-value y) (int-value z)) 6)) 
(check-sat) 
(get-model) 

(assert (not (value z))) 
(check-sat) 

Answer 2

有三個變量，我想這將是這樣的：

(define-fun cond_add ((cond Bool) (x Int) (sum Int)) Int 
    (ite cond (+ sum x) sum)) 
(declare-fun sum() Int) 
(assert (= sum (cond_add x x.val (cond_add y y.val (cond_add z z.val 0))))) 
(assert (> sum 6)) 

在這裏，我定義一個宏cond_add添加變量當相應的條件成立時，一個累加器。並且sum被定義爲基於x,y和z的真值來解釋條件總和x.val,y.val和z.val。