z3 反例中的数组元素

Question

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。 我可以添加不显示这些行的选项吗？

Answer 1

您将 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 变量。以这种方式混合两种输入语言只会造成很多混乱。