我在 Win10 x64、python 2.7 x64 中使用最新的 z3py
构建版本 (x64)。
当我尝试在此约束上调用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等
均为整数)
我注意到 check
对于这个约束产生空。
这是否意味着该约束不满足?
最佳答案
需要先调用check
,只有返回SAT才会有模型。
摘自@Christoph 的评论。
谢谢。
关于z3.z3types.Z3Exception : model is not available,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/41052492/