Я использую последнюю версию выпуска z3py
(x64) в Win10 x64, python 2.7 x64.z3.z3types.Z3Exception: модель недоступна
Когда я пытаюсь вызвать model
на это ограничение:
(i2 % 59) == (i2 * i10) , (i10 % 43) == ((i2 + i12) % 3) , 4 != (i14 % 28) ,
5 != (i14 % 28) , 6 != (i14 % 28) , 7 != (i14 % 28) , 8 != (i14 % 28) , (i2
- i12) >= (i12 + i10) , ((i2 - i1) - (i2 * i1)) >= (i1 - 50) , (i12 - i2) <
(i2 * i12)
Он бросает исключение z3.z3types.Z3Exception: model is not available
.
Все переменные (например i2, i10, etc
являются целыми числами)
Я отметил, что check
производят пустые для этого ограничения.
Означает ли это, что это ограничение является ненасытным?
Спасибо за помощь.
* Вы могли бы опубликовать весь исходный код? * –
'check' нужно вызвать сначала, и только если он вернет SAT, появится модель. –