Checking sat using check() with assumptions rises AttributeError: 'bool' object has no attribute 'as_ast'
Checking sat using check() with assumptions rises AttributeError: 'bool' object has no attribute 'as_ast'
为什么这有效：
>>> from z3 import *
>>> s = Solver()
>>> s.add([True])
>>> s.check()
sat
但这不是：
>>> from z3 import *
>>> s = Solver()
>>> s.check([True])
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "$HOME/.local/lib/python3.6/site-packages/z3/z3.py", line 6656, in check
_assumptions[i] = assumptions[i].as_ast()
AttributeError: 'bool' object has no attribute 'as_ast'
>>>
我错过了什么吗？我知道这是相同的操作，但没有将新约束记录到求解器中。
我使用的是 Z3 版本 4.8.6 - 64 位
正如您所指出的，确实没有充分的理由对此处的参数进行不同的处理。
由于 Python 的无类型特性，z3 绑定“玩”了一些技巧来解释您所写的内容，将它们转换成它可以使用的各种形式。对于s.add方法，它们比s.check()函数更“灵活”。
您可以通过以下方式解决此问题：
>>> from z3 import *
>>> s = Solver()
>>> s.check([Bool(True)])
sat
请注意，同样适用于 s.add：
>>> from z3 import *
>>> s = Solver()
>>> s.add([Bool(True)])
>>> print(s.check())
sat
因此，您可以通过以 add 和 check 都支持的形式编写布尔文字来“保持一致”。但理想情况下，方法本身在处理术语时应该是统一的。您已经发现了它们无缘无故不同的情况。
这不一定是 Python 中典型的“错误”：缺少静态类型迫使库开发人员支持无数种情况，并且很难在这样的设置中保持一切一致。但它绝对是一个疣。如果它真的给你带来麻烦，你可以在这里报告它：https://github.com/Z3Prover/z3/issues to see if there's someone who is concerned enough with this inconsistency to address it. (A pull-request fixing it will most likely be appreciated, the code is here.)
为什么这有效：
>>> from z3 import *
>>> s = Solver()
>>> s.add([True])
>>> s.check()
sat
但这不是：
>>> from z3 import *
>>> s = Solver()
>>> s.check([True])
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "$HOME/.local/lib/python3.6/site-packages/z3/z3.py", line 6656, in check
_assumptions[i] = assumptions[i].as_ast()
AttributeError: 'bool' object has no attribute 'as_ast'
>>>
我错过了什么吗？我知道这是相同的操作，但没有将新约束记录到求解器中。
我使用的是 Z3 版本 4.8.6 - 64 位
正如您所指出的，确实没有充分的理由对此处的参数进行不同的处理。
由于 Python 的无类型特性，z3 绑定“玩”了一些技巧来解释您所写的内容，将它们转换成它可以使用的各种形式。对于s.add方法，它们比s.check()函数更“灵活”。
您可以通过以下方式解决此问题：
>>> from z3 import *
>>> s = Solver()
>>> s.check([Bool(True)])
sat
请注意，同样适用于 s.add：
>>> from z3 import *
>>> s = Solver()
>>> s.add([Bool(True)])
>>> print(s.check())
sat
因此，您可以通过以 add 和 check 都支持的形式编写布尔文字来“保持一致”。但理想情况下，方法本身在处理术语时应该是统一的。您已经发现了它们无缘无故不同的情况。
这不一定是 Python 中典型的“错误”：缺少静态类型迫使库开发人员支持无数种情况，并且很难在这样的设置中保持一切一致。但它绝对是一个疣。如果它真的给你带来麻烦，你可以在这里报告它：https://github.com/Z3Prover/z3/issues to see if there's someone who is concerned enough with this inconsistency to address it. (A pull-request fixing it will most likely be appreciated, the code is here.)