Z3: Extraire des valeurs-modèles existentielles

Question

Je joue avec le solveur QBVF de Z3 et je me demande s'il est possible d'extraire des valeurs d'une assertion existentielle. À savoir, disons que je donne les résultats suivants:

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x)))) 

Cela dit essentiellement qu'il ya un « moins » valeur 16 bits non signé. Ensuite, je peux dire:

(check-sat) 
(get-model) 

Et Z3-3.0 répond joyeusement:

sat 
(model (define-fun x!0() (_ BitVec 16) 
#x0000) 
) 

Ce qui est vraiment cool. Mais ce que je veux faire, c'est pouvoir extraire des pièces de ce modèle via la valeur d'acquisition. Sans surprise, aucun des éléments suivants semblent fonctionner

(get-value (x)) 
(get-value (x!0)) 

Dans chaque cas Z3 se plaint à juste titre il n'y a pas une telle constante. Clairement Z3 a cette information comme en témoigne la réponse à l'appel (check-sat). Est-il possible d'accéder automatiquement à la valeur existentielle via get-value, ou un autre mécanisme?

Merci ..

Answer 1

Dans Z3, get-value permet uniquement à l'utilisateur de référencer les déclarations « globales ». La variable existentielle x est une déclaration locale. Ainsi, il ne peut pas être accédé en utilisant get-value. Par défaut, Z3 élimine les variables existentielles en utilisant un processus appelé "skolemization". L'idée est de remplacer les variables existentielles par de nouvelles constantes et symboles de fonction. Par exemple, la formule

exists x. forall y. exists z. P(x, y, z) 

est converti en

forall y. P(x!1, y, z!1(y)) 

Notez que z devient fonction parce que le choix de z peut dépendre y. Wikipedia a une entrée sur skolem normal form

Cela étant dit, je n'ai jamais trouvé une solution satisfaisante pour le problème que vous avez décrit. Par exemple, une formule peut avoir plusieurs variables existentielles avec le même nom. Ainsi, il n'est pas clair comment référencer chaque instance dans la commande get-value de manière non ambiguë.

Une solution de contournement possible pour cette limitation est d'appliquer l'étape de skolemization "à la main", ou au moins pour les variables dont vous voulez connaître la valeur. Par exemple,

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x)))) 

est écrit que:

(declare-const x (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y x))) 
(check-sat) 
(get-value x) 

Si la variable existentielle est niché dans un quantificateur universel tel que:

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x)))) 
(check-sat) 
(get-model) 

Une fonction frais Skolem peut être utilisé pour obtenir la valeur de x pour chaque y. L'exemple ci-dessus devient:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 
(check-sat) 
(get-model) 

Dans cet exemple, sx est la fonction nouvelle. Le modèle, produit par Z3, attribuera une interprétation pour sx. Dans la version 3.0, l'interprétation est la fonction d'identité. Cette fonction peut être utilisée pour obtenir la valeur x pour chaque y.