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 

私は、変数を追加するマクロ cond_addを定義ここで

(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)) 

：

たぶん配列での作業は、私が何かのようにそれは想像、これを達成するための方法...三つの変数で

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

です対応する条件が成立したときのアキュムレータ。 sumは、真理値x,yおよびzに基づいて、x.val,y.valおよびz.valの条件付き合計を説明するように定義されています。