des questions Z3 QBVF

Question

Suite à la discussion précédente: Z3: Extracting existential model-values

Y at-il une différence entre:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

Et

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

En ce qui concerne Z3? C'est-à-dire, vais-je toujours obtenir le solveur QBVF pour ce dernier automatiquement?

En outre, sur l'expérimentation, je trouve que si j'ENJEU:

(eval (sx #x8000)) 

Après un appel (check-sat), il fonctionne très bien (ce qui est génial). Ce qui serait mieux est de savoir si je pouvais dire aussi:

(eval (sx (get-value (y)))) 

Hélas, pour cette requête Z3 se plaint que c'est un invalid function application. Est-il possible d'utiliser la fonction eval de cette manière?

Merci!

Answer 1

Les scripts

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 

et

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 

ne sont pas équivalents. Le second est en fait equisatisfiable à

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y)))) 

En ce qui concerne la commande eval, vous pouvez référencer une constante et non interprétée symbole de fonction. Ainsi, vous pouvez écrire:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(declare-fun y() (_ BitVec 16)) 
(assert (bvuge y (sx y))) 
(check-sat) 
(eval (sx y)) 

La commande (eval (sx y)) ne fonctionne pas pour le premier script, car y est une variable universelle.