Utiliser différents solveurs dorsaux en Z3

Question

J'utilise l'interface Z3 Python pour créer des formules pour mes expériences. J'envoie alors cette formule à un solveur Z3. Si je suis correct, Z3 utilise son propre solveur! Comment utiliser un autre solveur SAT/SMT avec Z3py? La façon dont j'utilise pour le faire dans CBMC (C bounded model checker): Exécuter le programme et cracher une représentation intermédiaire DIMAC (dans un fichier), puis utiliser ce fichier comme une entrée pour d'autres solveurs SAT. Puis-je faire des choses similaires dans Z3. Je vous remercie.

Answer 1

Tous les solveurs SMT prennent en charge le format d'entrée SMT2, vous pouvez donc faire de même avec Z3 et d'autres solveurs SMT. Z3py peut traduire les objets Solver et Goal en chaînes conformes à SMT2 (certaines déclarations de variables compliquées, par exemple certains types de données peuvent être manquants).

Z3py est une API spécifique à Z3 (comme son nom l'indique) elle ne permet pas d'utiliser d'autres solveurs SMT.

Answer 2

On dirait que vous devriez vraiment utiliser une interface SMT agnostique de solveur au lieu de Z3py. Il y a eu plusieurs tentatives de créer de telles interfaces, avec des degrés variables de support pour de multiples solveurs:

• https://github.com/pysmt/pysmt est une API Python solveur agnostique solveurs SMT. Je ne l'ai pas utilisé moi-même, mais cela semble prometteur, surtout si vous voulez que Python soit votre API de plus haut niveau.

• https://github.com/sosy-lab/java-smt est un projet similaire qui utilise Java comme langage hôte. Est ma propre tentative de fournir une API agnostique de solveur pour l'utilisation de solveurs SMT, celle-ci écrite dans Haskell.

Ce n'est en aucun cas une liste exhaustive. Je suis sûr qu'il y en a d'autres, dans divers langages d'accueil, avec des degrés de maturité différents. Le choix dépend en grande partie de la préférence de votre langue d'hôte et des fonctionnalités offertes par chaque système; qui peut varier largement.