Как я могу использовать Z3Py DLL?

Question

Я пытался использовать dll Z3Py, но это не сработало.Вот мои тестовые программы и ошибки.Я очень плохо знаком с Python, я думаю, что пропустил какую-то важную часть, которую все уже знают.

init("z3.dll")

Traceback (most recent call last):
File "test5.py", line 1, in <module>
    init("z3.dll")

NameError: имя 'init' не определено

введите описание изображения здесь

введите описание изображения здесь

Я также попробовал другой способ загрузить dll:

import ctypes
so = ctypes.WinDLL('./z3.dll')     #for windows
print(so)
s = Solver()

<WinDLL './z3.dll', handle 10000000 at 0x10b15f0>
Traceback (most recent call last):
  File "test5.py", line 5, in <module>
    s = Solver()
NameError: name 'Solver' is not defined

введите описание изображения здесь

введите описание изображения здесь

Answer 1

Как правило, все, что вам нужно сделать, это импортировать z3:

from z3 import *

s = Solver()
x = Int("x")
s.add(x > 5)
s.check()
print s.model()

Что происходит, когда вы запускаете этот простой скрипт?