向 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 本身附带的东西，因此您必须从其他第三方获取它，或者可能是您自己编写的。如果不知道它是如何定义的，堆栈溢出上的任何人都不可能为您提供任何指导。

无论如何，正如您怀疑的那样，您无法将其结果反馈给 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 语法本身的现有支持之外的任何内容都将需要大量的工作。