时间戳

首页 > 解决方案 > 如何在 Z3 Solver/theorem Prover 下获取未解释排序的常量和特定实例？

z3 - 如何在 Z3 Solver/theorem Prover 下获取未解释排序的常量和特定实例？

问题描述

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，y，z，w”可以是block1或block2，这取决于我们为下一个设置的约束Solver().add()，但现在我希望常量“x，y，z，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, y, z, w = Consts('x y z w', BlockType) # constants(a.k.a variables of BlockType)

标签： z3z3pytheorem-proving

解决方案

我不太清楚你到底在问什么，但看起来你想要一个始终固定为一个值的枚举常量？（类似于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]

推荐阅读