Utilisez Z3 et smtlib pour calculer la configuration / le modèle avec des valeurs mixtes

Question

Comment calculer les valeurs attribuées? Voici un exemple:

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

Avec cela, j'aurais 2 modèles:

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

Maintenant, ce que je veux, c'est quelque chose comme ça:

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

Je voudrais donc obtenir le modèle où la somme des attributs est supérieure à 6:

x=true and z=true

Peut-être que travailler avec des tableaux est un moyen d'y parvenir ...

Answer 1

Je ne sais pas si j'ai bien compris votre question. Il semble que vous souhaitiez associer un attribut (entier) à chaque variable booléenne. Ainsi, chaque variable est une paire: une valeur booléenne et un attribut entier. Je suppose que par sum, vous entendez la somme des attributs des variables affectées à true. Si tel est le cas, vous pouvez le modéliser en Z3 de la manière suivante:

;; 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

Avec trois variables, j'imagine que ce serait quelque chose comme:

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

Ici, je définis une macro cond_add pour ajouter une variable à un accumulateur lorsqu'une condition correspondante se vérifie.Et sum est défini pour tenir compte de la somme conditionnelle de x.val, y.val et z.val en fonction des valeurs de vérité de x, y et z.