如何在 Z3 求解器/定理证明器下获得未解释排序的常量和特定实例？

如何解决如何在 Z3 求解器/定理证明器下获得未解释排序的常量和特定实例？

x_instance = IntVal('3')
x_uninterpred_const1 = Const("x",IntSort())
x_uninterpred_const2 = Int("x")# syntax sugar for the former line above

在 Z3 中，我们使用术语“变量”来表示通用变量和存在变量。无量词公式不包含变量，只包含常量。但至少我们可以同时得到一个值为3的int_instance。

然后当我将 Z3 用于 Blockworld 时，我发现了这一点：

BlockType,(block1,block2) = EnumSort('Block',('block1','block2'))
x,y,z,w = Consts('x y z w',BlockType)

我认为这意味着常量 "x,w" 可以是 block1 或 block2，这取决于我们为下一个 Solver().add() 设置的约束，但现在我想要常量 "x,w" 成为无数块，即使我还没有“枚举”所有可能的块实例，如“A，B，C，D，...”。

但现在我只有两个特定的块实例名称“block1,block2”。我怎样才能在 Z3 求解器中得到这个？ （就像上面的 IntVal("3") 和 IntSort 常量一样）

我写了下面的代码，但我认为它不正确：

BlockType = DeclareSort('Block type')#Uninterpreted or free Sorts"BlockType",block1,block2 = Consts('blockinstance1 blockinstance2',BlockType) #this seems wrong but I do not know how to write. #I do not how to get this: I want two specific block but not constants(a.k.a variables of BlockType)
x,BlockType) # constants(a.k.a variables of BlockType)

解决方法

我不太清楚你到底在问什么，但看起来你想要一个总是固定在一个值的枚举常量？ （类似于 IntVal 对整数的作用。）

为此，只需在求解器中断言相等即可：

from z3 import *

BlockType,(block1,block2) = EnumSort('Block',('block1','block2'))

s = Solver()
x = Const('x',BlockType)
s.add(x == block1)
print(s.check())
print(s.model())

打印：

sat
[x = block1]