Как использовать dll Z3Py?

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

init("z3.dll")

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

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

Как использовать dll Z3Py?

Я также пробовал другой способ загрузить 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

Как использовать dll Z3Py?

python dll z3 smt z3py

27.10.2018 05:58

Почему в Python есть оператор "pass"?

Оператор pass в Python - это простая концепция, которую могут быстро освоить даже новички без опыта программирования.

Некоторые методы, о которых вы не знали, что они существуют в Python

Python - самый известный и самый простой в изучении язык в наши дни. Имея широкий спектр применения в области машинного обучения, Data Science,...

Основы Python Часть I

Вы когда-нибудь задумывались, почему в программах на Python вы видите приведенный ниже код?

LeetCode - 1579. Удаление максимального числа ребер для сохранения полной проходимости графа

Алиса и Боб имеют неориентированный граф из n узлов и трех типов ребер:

Оптимизация кода с помощью тернарного оператора Python

И последнее, что мы хотели бы показать вам, прежде чем двигаться дальше, это

Советы по эффективной веб-разработке с помощью Python

Как веб-разработчик, Python может стать мощным инструментом для создания эффективных и масштабируемых веб-приложений.

161

Перейти к ответу Данный вопрос помечен как решенный

Ответы 1

Ответ принят как подходящий

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

from z3 import *

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

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

Оно работает. Я уже закончил свою программу с import z3. Теперь я хочу запустить его на компьютере без z3py, поэтому попробовал dll.

— 28.10.2018 12:41

Вы не можете этого сделать. DLL содержит основные функции Z3 (экспортированные из C++), но вам все равно нужно установить Z3py, чтобы иметь все функции оболочки. (Как класс Solver и все остальные питонические идиомы.)

— 28.10.2018 14:38

Большое спасибо. Значит, функция init () используется для загрузки ядра z3 после импорта? Как z3.init ()?

— 28.10.2018 15:36

Всякий раз, когда вы обращаетесь к функции Z3py, библиотека автоматически инициализирует DLL и делает доступными основные функции. Это происходит за кадром. В редких случаях (например, при нестандартной установке) вам может потребоваться явный вызов init, но это определенно не рекомендуемый способ. В любом случае на компьютере должен быть установлен интерфейс Z3py; просто наличия DLL недостаточно. Смотрите самый низ ericpony.github.io/z3py-tutorial/guide-examples.htm

— 28.10.2018 17:56

Вдохновленный вами, я думаю, что нашел способ запустить z3 без установленного z3py. Я нахожу файл библиотеки, копирую его в свой локальный каталог, переименовываю папку в «z3local» и импортирую их с помощью import z3local.z3 as z3. И тестовая программа работала отлично, даже если я удалил z3py.

— 28.10.2018 19:04

Это то, что я бы назвал нестандартной установкой. Если у вас нет веских причин поступить иначе, я бы не рекомендовал этого делать. (Во-первых, вам придется повторять то же самое для каждого нового выпуска / исправления ошибки в самом официальном z3.)

— 28.10.2018 19:13

Просто экспериментирую с Z3. Так что это не имеет большого значения. Одним словом, большое спасибо. Думаю, я действительно кое-что узнал о Python.

— 28.10.2018 19:19

27.10.2018 16:33