如何解决z3:将袋作为数组
下面的摘录来自z3的教程:https://rise4fun.com/z3/tutorialcontent/guide
(define-sort A () (Array Int Int Int))
(define-fun bag-union ((x A) (y A)) A
((_ map (+ (Int Int) Int)) x y))
(declare-const s1 A)
(declare-const s2 A)
(declare-const s3 A)
(assert (= s3 (bag-union s1 s2)))
(assert (= (select s1 0 0) 5))
(assert (= (select s2 0 0) 3))
(assert (= (select s2 1 2) 4))
(check-sat)
(get-model)
我无法理解此行的工作方式-((_ map (+ (Int Int) Int)) x y))
此外,我不明白,为什么在下面给定的输出中,从索引[1,2]而不是索引[0,0]为数组s2分配常量4的值:
sat
(model
(define-fun s2 () (Array Int Int Int)
(store ((as const (Array Int Int Int)) 4) 0 0 3))
(define-fun s1 () (Array Int Int Int)
((as const (Array Int Int Int)) 5))
(define-fun s3 () (Array Int Int Int)
(store ((as const (Array Int Int Int)) 9) 0 0 8))
)
我什至尝试将更多值添加到s2的其他索引中,但是z3只选择[1,2]索引处的值作为数组的常数。谁能解释发生了什么事?预先感谢。
解决方法
在z3中,map
是将点运算符扩展到数组的函数。
假设您有两个符号整数。您可以像这样添加它们:
(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 4))
如果有两个数组会发生什么? SMTLib没有指定“添加”两个数组的方法,即没有办法说给我一个新的数组,它是两个数组的逐点求和。这就是z3的map
扩展名的来源。您可以这样编写:
(declare-const arr1 (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const arr3 (Array Int Int))
(assert (= arr3 ((_ map (+ (Int Int) Int)) arr1 arr2)))
再次注意,这是一个z3
扩展名,不适用于其他SMT求解器。上面发生的事情是z3将在元素上添加arr1
和arr2
,并且由于arr3
而要求与arr3
等效。
(此外:在本教程示例中,他们正在对袋子建模;即,他们在地图中存储了两个整数;因此有点复杂。但是在其他方面想法是相同的。)
类型消歧需要在+
上使用有趣的字母。您可以这样看:(map + arr1 arr2)
。不幸的是,SMTLib的类型系统不够强大,无法确定您想要哪个+
,因为它是重载运算符。因此,您必须通过编写(_ map (+ (Int Int) Int))
来明确给出类型注释。这是相当令人困惑的语法,但是这就是您说我希望“ map”在这种情况下在“ +”上工作的方式。您几乎可以忽略它。
我不明白您问题的第二部分。求解器可以自由选择任何令人满意的模型。另外,请记住SMTLib数组 not 没有界限。即任何Int
是有效索引。 (这与许多编程语言中的数组形成对比。)如果您还有其他问题,请随时启动另一个线程。 (当每个线程问一个问题时,堆栈溢出的效果最好。)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。