相当于Z3Py中的（断言（= a 10））

Question

我正在创建带有某些节点的树。每个节点都有与其相关的某些属性，例如成本。想法是找到成本最低的路径。叶节点已经为其声明了成本。非叶子节点的成本将根据其子节点以最低的成本进行定义。我正在尝试编写用于定义叶节点成本的断言。

我有SMT-LIB 2.0标准中的工作代码。我看过适用于Z3的基于python的示例，但找不到解决方案。

注意：我对S3这样的SMT解算器非常陌生。

我知道我们可以简单地使用SMT-LIB 2.0标准编写(assert (= a 10))。对于Python，我尝试了a = IntVal("10")。我不确定这是否是我需要的。

我想使用Z3Py编写(assert (= a 10))类似代码。任何帮助将不胜感激。

Answer 1

在z3py中，这就是：

from z3 import *

s = Solver()

a = Int('a')

s.add(a == 10)

print s.check()
print s.model()

打印：

sat
[a = 10]

分配与平等

[在SMTLib或Z3py中编程时，最好将相等视为比较，而不是赋值。当你说：

(assert (= a 10))

在SMTLib中，您正在不是向a分配任何内容。您只是说a的值应等于10。实际上，表达式(= a 10)的类型为Bool，因此您可以等效地说：

(assert (= True (= a 10)))

这将是多余的，但它说明了这一点。

当然，混淆是SMTLib中的“平等比较”被称为=，但在Python中是==；更糟糕的是，=在Python中作为赋值是有意义的；但这并不意味着您要说的话。如果您熟悉函数式编程，可以将SMTLib / Z3Py程序视为不同类型的变量的集合以及有关它们之间关系的断言。

希望有帮助！提出具体问题总是比英文散文更好。随时发布可能令人困惑的代码段。