#python #smt #z3py
Вопрос:
Я новичок в решателе z3 smt.Я использую python API z3py.
У меня есть небольшой вопрос, касающийся вывода функции z3.solve ().что это значит, когда я вызываю z3.solve() по некоторым ограничениям и получаю [] в качестве вывода? Также не мог бы кто-нибудь сослаться на хорошую документацию, пожалуйста
Комментарии:
1. [] был бы пустой список python, верно?
Ответ №1:
Вам действительно нужно предоставить информацию, которая вызывает это, так как это действительно зависит от ваших ограничений. Но вот самый простой способ проиллюстрировать это поведение:
from z3 import *
z3.solve([])
Когда я запускаю это, я получаю:
[]
полагаю, именно это вы и видите. Это, по сути, означает, что ваша система тривиально выполнима для всех переменных; т. Е. Либо у вас нет ограничений, либо они не ограничивают модель каким-либо определенным образом. В приведенном выше нет ограничений, поэтому у нас есть «тривиальная» модель. Если вы сделаете что-то более интересное, скажите:
from z3 import *
a, b = Ints('a b')
z3.solve([a > b, b > 3])
тогда вы увидите более интересную модель:
[b = 4, a = 5]
Существует множество документации по z3, z3py и SMTLib в целом (которая описывает базовый язык, на котором говорят все решатели SMT).:
- Для z3 начните с https://rise4fun.com/z3/tutorial
- Для привязок z3 python используйте: https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- Общая информация о SMTLib: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
Обратите внимание, что z3 также может быть написан на многих других языках, включая C, C , Java, Scala и Haskell, и это лишь некоторые из них. Обычно гораздо проще работать на языке более высокого уровня, чем непосредственно с SMTLib или C-привязками с голыми костями. Python и Haskell (на мой взгляд) предоставляют абстракции самого высокого уровня для упрощения программирования z3, но то, какую среду вам следует выбрать, действительно зависит от ваших общих целей. (Хотя большинство привязок поддерживают программирование общих ограничений, они имеют разные уровни автоматизации и доступ к различным средствам z3.)