Z3 将数组的默认值设置为零 [英] Z3 set default value of array to zero

问题描述

我正在尝试求解数组表达式的模型，其中数组的默认值等于 0.

I am trying to solve models for array expressions, where default values for array is equal to 0.

例如，我试图解决这个例子，但我一直得到未知的结果

For example, I am trying to solve this example, but I get unknown results all the time

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (= (select arr x) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

推荐答案

Patrick 关于不使用量词的建议是正确的！他们会让你的生活更艰难.但是，您很幸运，因为 z3 支持您的用例的常量数组，这很常见.语法是:

Patrick's advice on not using quantifiers is spot on! They'll make your life harder. However, you're in luck, because z3 supports constant-arrays for your use case, which is quite common. The syntax is:

(assert (= arr ((as const (Array Int Int)) 0)))

这确保 arr 的所有条目都为 0；不需要量化，z3 在内部处理它就好了.

This makes sure arr will have all its entries as 0; no quantification needed and z3 handles it internally just fine.

因此，您的基准将是:

(declare-const arr (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const a Int)
(declare-const b Int)

(assert (= arr ((as const (Array Int Int)) 0)))

(assert (> a 0))
(assert (<= a 10))

(assert (= arr2 (store arr a 1337)))

(assert (> b 0))
(assert (<= b 10))


(assert (= (select arr2 b) 0))

(check-sat)
(get-model)

很快就解决了.这样，您可以让整个数组以0 开头，并修改您感兴趣的范围；可以照常依赖变量，不需要提前知道.

which is solved in no time. This way, you can have the entire array start with 0, and modify the range you're interested in; which can depend on variables as usual and is not required to be known ahead of time.

这篇关于Z3 将数组的默认值设置为零的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！