2
votes

Solveur Z3 installé mais je ne peux rien importer

J'ai installé le package z3-solver de PyPi dans mon environnement Python3 à l'aide d'Anaconda Prompt (pip install z3-solver) et c'est tout.
Le package apparaît dans le répertoire site-packages / (le package contient _init__.py et tous les fichiers essentiels, y compris z3.py). Cependant, lorsque j'ai essayé d'exécuter cet exemple à partir de Jupyter Notebook, il renvoie le message suivant: NameError : le nom «Int» n'est pas défini.
Je n'ai utilisé Anaconda que pendant une courte période, donc je ne suis pas sûr du fonctionnement de l'installation. C'est vraiment étrange car la commande «pip install» fonctionne bien la plupart du temps. Ai-je fait quelque chose de mal ou ce package nécessite plus de configuration?

python conda anaconda z3

4 commentaires

Changer Int en int

Ça ne marche pas. Int est une classe définie dans z3 et l'exemple que j'ai utilisé est tiré de leur référentiel Github officiel, il n'est donc pas conforme à la syntaxe.

Avez-vous un fichier nommé z3.py dans le z3.py de votre projet?

Avez-vous suivi les recommandations d'utilisation de pip avec Conda? Voir, par exemple: anaconda.com/using-pip-in-a-conda-environment .

3 Réponses :

1
votes

Vous pouvez exécuter conda install pip , puis exécuter pip install z3-solver .

0 commentaires

1
votes

Désolé pour la mise à jour tardive.

J'ai réussi à résoudre le problème sur la base de ce guide .

Pour changer définitivement la variable sys.path dans Anaconda, j'ai créé un .PTH file qui contient le chemin vers z3 et z3 mis dans le répertoire site-packages .

Vous devrez peut-être copier le fichier libz3.dll dans le bon répertoire pour qu'il fonctionne. L'exécution de pip install z3-solver télécharge les fichiers requis et les place dans des packages de site, mais je ne peux pas importer z3 de n'importe où.

Peut-être que vous devez également réparer le chemin après avoir utilisé pip pour qu'Anaconda puisse le reconnaître. J'ai tout fait manuellement, donc je ne sais pas pourquoi pip ne fonctionne pas dans ce cas.

C'est tout ce que j'ai fait pour installer z3 sur mon Windows . J'espère que cela aide !

0 commentaires

0
votes

vous devez écrire:

from z3 import *
 
def main(): 
    
    s = Solver()
    x = Int('x')
    y = Int('y')
    s.add(x < 10)

qui a résolu mon NameError: name 'Solver' is not defined Exception

conditions préalables:

pip install z3
pip install z3-solver

exemple de code

from z3 import *

0 commentaires