时间戳

首页 > 解决方案 > z3 反例中的数组元素

z3 - z3 反例中的数组元素

问题描述

z3 工具的 aaary 元素的反例输出

我尝试以下python代码，并得到一个反例

from z3 import Solver, parse_smt2_string
s = Solver()
#str1="(declare-const x Int) (declare-const y Int) (declare-const z Int) (declare-const a1 (Array Int Int)) (declare-const a2 (Array Int Int)) (declare-const a3 (Array Int Int))  (assert (= (select a1 x) x)) (assert (= (store a1 x y) a1))"
str1="(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))"
s.add(parse_smt2_string(str1))
s.check()
m = s.model()    
for d in m:     
  print(d,m[d])
if str(s.check())=="sat":  
    print(s.model())  
    m = s.model()    
    for d in m: 
        print(d,m[d])


(s2, [(1, 2) -> 4, (0, 0) -> 3, else -> 7719])
(s3, [(1, 2) -> 8859, (0, 0) -> 8, else -> 8955])
(s1, [(1, 2) -> 8855, (0, 0) -> 5, else -> 1236])
(k!1, [(1, 2) -> 4, (0, 0) -> 3, else -> 7719])
(k!2, [(1, 2) -> 8859, (0, 0) -> 8, else -> 8955])
(k!0, [(1, 2) -> 8855, (0, 0) -> 5, else -> 1236])
....

(k!1, [(1, 2) -> 4, (0, 0) -> 3, else -> 7719]) 之类的行让我感到困惑？它们似乎是重复的行 (s2, [(1, 2) -> 4, (0, 0) -> 3, else -> 7719。我可以添加一个不显示这些行的选项吗？

标签： z3smt

解决方案

您将 SMTLib 和 Python 输入混合在一起；确实没有充分的理由这样做。使用 Python 或 SMTLib 编写程序。当您以这种方式使用 z3 时，您将无法访问已定义的变量。如果你直接在 z3py 中编程，那么你可以轻松地查询你定义的变量的值。除此之外，您最好的选择是简单地检查名称是否符合格式并在循环中k!n跳过它。for

另请注意，这些“辅助”模型变量的输出中将打印的内容完全取决于 z3 版本。当我使用来自 github 源的最新版本的 z3 运行您的程序时，它会打印：

(s2, Store(K(Int, 4), 0, 0, 3))
(s1, K(Int, 5))
(s3, Store(K(Int, 9), 0, 0, 8))
[s2 = Store(K(Int, 4), 0, 0, 3),
 s1 = K(Int, 5),
 s3 = Store(K(Int, 9), 0, 0, 8)]
(s2, Store(K(Int, 4), 0, 0, 3))
(s1, K(Int, 5))
(s3, Store(K(Int, 9), 0, 0, 8))

其中没有提到k!n变量。以这种方式混合两种输入语言只会造成很多混乱。

推荐阅读