Z3: Une meilleure façon de modéliser?

Question

J'ai deux instances de problèmes SMT. Le premier est ici:

http://gist.github.com/1232766 

Z3 retourne un modèle pour ce problème dans environ 2 minutes sur ma machine pas si grande, ce qui est génial .. J'ai aussi celui-ci:

http://gist.github.com/1232769 

J'ai couru z3 pendant la nuit sur ce problème, sans Z3 complétant. Si vous vérifiez le contenu de ces fichiers, vous verrez que le second est identique au premier, sauf qu'il a une assertion supplémentaire pour "rejeter" le modèle retourné par la première instance. (Vous pouvez faire un "diff" entre eux pour voir ce que je veux dire.) Je sais que ce problème a plusieurs modèles satisfaisants, et j'essaie d'utiliser z3 pour trouver tous les modèles satisfaisants. Je comprends que cela pourrait être complètement attendu, mais j'étais curieux de savoir pourquoi le second est un problème beaucoup plus difficile pour Z3 par rapport à la première. Y a-t-il une meilleure façon de formuler le deuxième problème afin que Z3 ait un temps plus facile?

Merci ..

Answer 1

Il est difficile de vous donner une réponse précise sans en savoir plus au sujet de votre application. Comme vous l'avez suggéré, la modélisation joue un grand rôle dans la logique que vous utilisez: AUFBV. La stratégie utilisée par Z3 a également un impact important sur la performance globale. Z3 est équipé de plusieurs stratégies intégrées. Il a beaucoup de paramètres qui peuvent être utilisés pour influencer la recherche. Z3 dispose également d'un langage de spécification de stratégie. C'est une nouvelle fonctionnalité. Je ne fais pas de publicité parce que ça marche, et le langage changera probablement dans les prochaines versions. Vous pouvez accéder à plus d'informations sur la langue de la stratégie en exécutant les commandes:

(help check-sat-using) 
(help-strategy) 

Cela étant dit, il y a une stratégie en Z3 builtin qui semble être efficace sur votre problème. C'est la stratégie utilisée pour la logique UFBV. Votre problème utilise des tableaux, mais ils peuvent être évités en transformant table0 en fonction avec deux arguments:

(declare-fun table0 ((_ BitVec 64) (_ BitVec 64)) (_ BitVec 8)) 

et remplace tous les termes de la forme (select (table0 s65) t) avec (table0 s65 t) où t est un terme arbitraire. Enfin, vous devez également ajouter la commande (set-logic UFBV) au début du fichier. Avec ce paramètre, j'ai réussi à générer 4 modèles différents pour votre requête. Je n'ai pas essayé de générer plus que ça. Chaque appel a consommé environ 75 secondes.