使用 check() 检查 sat 并假设上升 AttributeError: 'bool' object has no attribute 'as_ast' [英] Checking sat using check() with assumptions rises AttributeError: 'bool' object has no attribute 'as_ast'

问题描述

为什么会这样:

<预><代码>>>>从 z3 导入 *>>>s = 求解器()>>>s.add([真])>>>s.check()坐

但这不会:

<预><代码>>>>从 z3 导入 *>>>s = 求解器()>>>s.check([真])回溯(最近一次调用最后一次):文件<stdin>"，第 1 行，在 <module> 中.文件$HOME/.local/lib/python3.6/site-packages/z3/z3.py"，第 6656 行，检查_假设[i] = 假设[i].as_ast()AttributeError: 'bool' 对象没有属性 'as_ast'>>>

我错过了什么吗?我知道这是相同的操作，但没有将新约束记录到求解器中.

我使用的是 Z3 版本 4.8.6 - 64 位

解决方案

正如您所指出的，这里确实没有充分的理由对参数进行不同的处理.

由于 Python 的无类型特性，z3 绑定播放"了通过将它们转换为可以使用的各种形式来解释您所写内容的技巧.对于 s.add 方法，它们更灵活"；比 s.check() 函数.

你可以通过写来解决它:

>>>从 z3 导入 *>>>s = 求解器()>>>s.check([布尔(真)])坐

请注意，s.add 也是如此:

>>>从 z3 导入 *>>>s = 求解器()>>>s.add([布尔(真)])>>>打印(s.check())坐

因此，您可以保持一致"；通过以 add 和 check 支持的形式编写布尔文字.但理想情况下，这些方法本身在处理术语时应该是统一的.您发现了一种情况，它们无缘无故地不同.

这不一定是错误"，这在 Python 中很典型:缺乏静态类型迫使库开发人员支持无数种情况，并且很难在这样的设置中保持所有内容一致.但它绝对是一个疣.如果它真的给你带来了麻烦，你可以在这里报告它:https://github.com/Z3Prover/z3/issues 看看是否有人对这种不一致感到足够关注来解决它.(修复它的拉取请求很可能会受到赞赏，代码是 此处.)

Why this works:

>>> from z3 import *
>>> s = Solver()
>>> s.add([True])
>>> s.check()
sat

but this doesn't:

>>> 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'
>>>

Am I missing something? I understood that it was the same operation but without recording the new constraints into the solver.

I am using Z3 version 4.8.6 - 64 bit

解决方案

As you are pointing out, there's really no good reason for the treatment of arguments differently here.

Due to the untyped nature of Python, z3 bindings "play" tricks to interpret what you wrote by casting them into various forms it can work with. For the s.add method, they are more "flexible" than the s.check() function.

You can work around it by writing:

>>> from z3 import *
>>> s = Solver()
>>> s.check([Bool(True)])
sat

Note that the same works with s.add too:

>>> from z3 import *
>>> s = Solver()
>>> s.add([Bool(True)])
>>> print(s.check())
sat

So, you can be "consistent" by writing boolean literals in a form that's supported by both add and check. But ideally, the methods themselves should be uniform in their handling of terms. You've found a case where they differ for no good reason.

This isn't necessarily a "bug," as is typical in Python: Lack of static types force library developers to support myriad of cases, and it's hard to keep everything consistent in such a setting. But it definitely is a wart. If it's really causing you trouble, you can report it as such here: 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.)

这篇关于使用 check() 检查 sat 并假设上升 AttributeError: 'bool' object has no attribute 'as_ast'的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！