python - 将二元运算符添加到 z3

Question

我正在尝试解析字符串并将其转换为等效的 z3 形式。

import z3

expr = 'x + y = 10'

p = my_parse_expr_to_z3(expr)  # results in: ([x, '+', y], '==', [10]) 
p = my_flatten(p)              # after flatten: [x, '+', y, '==', 10]

解析字符串的类型检查:

for e in p:    
    print(type(e), e)   

# -->
      <class 'z3.z3.ArithRef'>   x
      <class 'str'>              +   
      <class 'z3.z3.ArithRef'>   y
      <class 'str'>              ==
      <class 'int'>              10
     

当我现在尝试:

s = z3.Solver()
s.add(*p)

我得到:

Traceback (most recent call last):
  File "<input>", line 1, in <module>
  File "...\venv\lib\site-packages\z3\z3.py", line 6938, in add
    self.assert_exprs(*args)
  File "..\venv\lib\site-packages\z3\z3.py", line 6926, in assert_exprs
    arg = s.cast(arg)
  File "..\venv\lib\site-packages\z3\z3.py", line 1505, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "..\venv\lib\site-packages\z3\z3.py", line 112, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

等号和加号碰巧是错误的类型/用法？我怎样才能正确翻译它？

Answer 1

parse_expr_to_z3 的定义从何而来？它绝对不是 z3 本身附带的东西，因此您必须从其他第三方获得它，或者您可能自己编写了它。在不知道它是如何定义的情况下，stack-overflow 上的任何人都不可能为您提供任何指导。

无论如何，正如你所怀疑的那样，它的结果不是你可以反馈给 z3 的东西。它失败正是因为您可以添加到求解器的内容必须是约束，即 z3 中 Bool 类型的表达式。显然，这些成分都没有这种类型。

所以，长话短说，这个 parse_expr_to_z3 似乎并没有按照您的意图设计。有关预期用例的更多详细信息，请联系其开发人员。

如果您尝试将断言从字符串加载到 z3，那么您可以使用所谓的 SMTLib 格式来执行此操作。像这样的东西:

from z3 import *

expr = """
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
"""

p = parse_smt2_string(expr)

s = Solver()
s.add(p)
print(s.check())
print(s.model())

这打印:

sat
[y = 0, x = 10]

您可以在 https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf 中找到更多关于 SMTLib 语法的信息

请注意，尝试使用任何其他语法(如您建议的 'x + y = 10')执行此操作将需要了解字符串中的变量 (x 和 y 在这种情况下，但当然可以是任意的)，以及什么样的符号(+ 和 = 在你的情况下，但同样可以是任意数量的不同符号)及其确切含义。在不知道您的确切需求的情况下，很难发表意见，但使用现有的 SMTLib 语法本身支持以外的任何东西都需要大量的工作。