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， 否则 -> 7719]( 之类的行让我感到困惑？ 它们似乎是重复的行 (s2， [(1， 2( -> 4， (0， 0( -> 3， 否则 -> 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变量。以这种方式混合两种输入语言只会造成很多混乱。