Quelqu'un sait comment convertir un bitvector signé en int signé en Z3?
(> (bv2int (bvxor ((_ int2bv 32) x1) ((_ int2bv 32) y1))) 0)x1 et y1 est deux signé int, et après le XOR. Comment puis-je les convertir en int signé?
Vous pouvez utiliser int2bv et bv2int, mais pour la plupart, ces fonctions seront traitées comme non interprétées (voir par exemple API doc). Si vous avez besoin de la sémantique réelle, vous devrez les implémenter vous-même. Ce n'est pas du tout difficile (juste une grosse somme sur les termes if-then-elses de 2^i*x1[i]), mais les contraintes que vous obtenez de cette façon sont fortement non-linéaires, donc il est probable que la théorie des nombres entiers abandonnera et retournera inconnue. Voir par exemple Z3 Performance with Non-Linear Arithmetic, How does Z3 handle non-linear integer arithmetic? et Z3 : Questions About Z3 int2bv?.