将二元运算符添加到 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 语法本身的支持以外的任何东西都需要大量的工作。