Support pour AUFBV?

Question

Est-ce que Z3 supportera AUFBV?

Pour le script suivant:

(set-logic AUFBV) 
(declare-fun x() (_ BitVec 16)) 
(declare-const t (Array (_ BitVec 16) (_ BitVec 16))) 
(assert (= (select t #x0000) #x0000)) 

La démo Z3 en ligne semble être satisfait de l'appel set-logic, mais il se plaint des sortes BitVec et Array. (Soit dit en passant, la démo en ligne semble être satisfait de l'appel set-logic quel que soit le nom logique, même avec des noms fictifs tels que (set-logic blarg).)

Le site web SMT-Lib ne mentionne pas ni UFBV ni AUFBV, mais étant donné leurs homologues sans quantificateur (QF_UFBV et QF_AUFBV), j'espérais que Z3 supporterait aussi AUFBV.

Inutile de dire que les tableaux jouent un rôle très important dans la pratique. Je pense que la logique de l'AUFBV devrait rester décidable étant donné l'argument de la finitude. Ce serait vraiment agréable de voir Z3 le supporter.

Merci!

Answer 1

Z3 utilise la commande set-logic pour se configurer. Si un script SMT ne contient pas le set-logic, tous les solveurs théoriques sont activés. Si vous supprimez la commande set-logic de votre script, alors Z3 fonctionnera comme prévu.

Comme vous l'avez dit, la logique AUFBV est décidable. Cependant, la complexité est vraiment élevée (NEXPTIME-complete). En théorie, le module MBQI (Instanciation basée sur un modèle de quantificateur) garantit que Z3 est une procédure de décision pour cette logique, mais en raison de la complexité élevée, Z3 échouera (exécution sans mémoire et/ou temps) dans de nombreux scripts.

La logique AUFBV ne figure pas dans la liste des logiques officiellement supportées. Z3 ne l'a pas reconnu et n'a pas installé de solutionneur théorique. Donc, pour utiliser cette logique dans Z3 3.1, vous ne devriez pas utiliser la commande set-logic.

BTW, vous n'avez pas vraiment besoin de tableaux. Ils peuvent être encodés en UFBV en utilisant des quantificateurs. Dans de nombreux cas, si l'on utilise des quantificateurs, il est préférable d'éviter la théorie des réseaux. Le solveur de la théorie des réseaux de Z3 est optimisé pour les problèmes sans quantificateur.

En ce qui concerne les commandes bidon telles que (set-logic blarg), j'ai ajouté du code pour afficher un message d'avertissement disant que la logique n'a pas été reconnue, et Z3 utilisera toutes les théories disponibles. La modification sera disponible en Z3 3.2. J'ai également inclus AUFBV dans la liste des logiques officiellement supportées.