0

我有以下查询（使用 SMT-LIB v1.0 标准编写）：

(benchmark gametime
:status unknown
:logic QF_AUFBV
:extrafuns ((x  BitVec[32]))
:extrafuns ((a  Array[32:32]))
:extrapreds ((constraint1 ))
:extrapreds ((constraint0 ))
:formula
(flet ($x37 (and (iff constraint0 (= (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32]))))
(and $x37 (and constraint0 constraint1)))
)

（查询有点多余，但它是自动生成的。）

通过 Z3 运行它，并要求一个模型，我收到以下信息：

a -> as-array[k!0]
constraint1 -> true
x -> bv1[32]
constraint0 -> true
k!0 -> {
  bv0[32] -> bv0[32]
  else -> bv0[32]
}

这很好，因为我根据需要有“a”和“x”的值。然而，另一个查询是类似的，除了一个小的变化：

(benchmark gametime
:status unknown
:logic QF_AUFBV
:extrafuns ((x  BitVec[32]))
:extrafuns ((a  Array[32:32]))
:extrapreds ((constraint1 ))
:extrapreds ((constraint0 ))
:formula
(flet ($x37 (and (iff constraint0 (**bvuge** (select a bv0[32]) bv0[32])) (iff constraint1 (= x bv1[32]))))
(and $x37 (and constraint0 constraint1)))
)

更改突出显示：什么是相等现在是“bvuge”检查。我从 Z3 收到以下型号：

constraint1 -> true
x -> bv1[32]
constraint0 -> true

我不再有“a”的任务了。这是故意的吗？如果模型中不存在我应该假设的变量的“默认”值吗？（例如，这里的默认值是数组“a”处处为零。）

对于它的价值，这个问题只有在操作是“bvuge”时才会出现。其他（“bvsge”、“bvugt”、“bvsgt”、“bvult”、“bvslt”、“bvule”、“bvsle”）似乎有效。

4

1 回答 1

1

我不再有“a”的任务了。这是故意的吗？

是的，这是故意的。数组的任何值都将满足公式。这是因为约束 0：

   (bvuge (select a bv0[32]) bv0[32]))

等价于真。在无符号比较下，任何位向量值都大于或等于 0。所以'a'的值是无关紧要的。

于 2013-01-24T20:26:04.413 回答