我正在尝试求解数组表达式的模型,其中数组的默认值等于 0。
例如,我正在尝试解决这个例子,但我总是得到未知的结果
(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)
帕特里克关于不使用量词的建议是正确的!他们会让你的生活变得更加艰难。不过,您很幸运,因为 z3 支持您的用例的常量数组,这很常见。语法是:
(assert (= arr ((as const (Array Int Int)) 0)))
这可以确保arr
其所有条目将作为0
;不需要量化,z3 在内部处理得很好。
因此,您的基准将是:
(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
,并修改您感兴趣的范围;它可以像往常一样依赖于变量,并且不需要提前知道。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)