Пустая модель в z3
z3py snippet:
x = Int('x') s = Solver() s.add(x <= x) print s.check() print s.model() print s.model().sexpr() http://rise4fun.com/Z3Py/mfPU
Вывод:
sat []
Любое значение x будет делать, но z3 возвращает пустую модель. Имеет ли отсутствующая свободная переменная x в модели, указывает, что любое целочисленное значение является допустимой моделью?
- Хеширование выражений в Z3Python
- Обучение Z3py – есть поддержка массивов и циклов
- Windows: Z3Exception («init (Z3_LIBRARY_PATH) должен быть вызван перед использованием Z3-python»)
- Python – Оптимизация системы неравенств
- Решение формул параллельно с z3
Да, в Z3, если константа (такая как x ) не появляется в модели, то это «не заботится». То есть любое значение x удовлетворяет формуле. При оценке значения константы мы можем включить «завершение модели». То есть Z3 будет использовать произвольную интерпретацию для символов «не заботясь». Вот пример http://rise4fun.com/Z3Py/bvVO
x = Int('x') s = Solver() s.add(x <= x) print s.check() m = s.model() print m.evaluate(x) print m.evaluate(x, model_completion=True) print m