1

我尝试形式化一个以数组和数组列表作为参数的函数，并返回列表中数组的索引。我尝试了非常不同的方法并从 Z3 获得了“未知”。

这是我尝试的一些代码，其中第一个和第二个公理都不起作用（以及其他几个我没有在这里包含的代码）：

(declare-fun SameArray ((Array Int Real) (Array Int Real)) Bool)
(declare-fun Match ((Array Int Real) (Array Int (Array Int Real))) Int)

(assert (forall ((array1 (Array Int Real)) (array2 (Array Int Real)))
    (= 
      (SameArray array1 array2)
      (ite (forall ((i Int)) (= (select array1 i) (select array2 i) )) true false)
    )
  ) 
)

;(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real))) )
;  (or
;    (exists ((index Int))
;      (and
;        (= (SameArray pattern (select list index)) true)
;        (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index)))
;        (= (Match pattern list) index)
;      )
;    )
;    (= (Match pattern list) (- 1))
;  )
;))

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real))) )
  (exists ((index Int))
    (and
      (= (Match pattern list) index)
      (or
        (and
          (= (SameArray pattern (select list index)) true)
          (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index)))
        )
        (= index (- 1))
      )
    )
  )
))

; Testing - SameArray

(declare-const a1 (Array Int Real))
(declare-const a2 (Array Int Real))

(assert (= (store a1 1 1.1) a1))
(assert (= (store a1 2 1.2) a1))
(assert (= (store a1 3 1.3) a1))

(assert (= (store a2 1 2.1) a2))
(assert (= (store a2 2 2.2) a2))
(assert (= (store a2 3 2.3) a2))

(assert (= (SameArray a1 a1) true))
(assert (= (SameArray a1 a2) false))

(check-sat)

; Testing - Match

(declare-const aAll (Array Int (Array Int Real)) )

(assert (= (store aAll 1 a2) aAll))
(assert (= (store aAll 2 a1) aAll))

(assert (= (Match a1 aAll) 2))

(check-sat)

编辑：即使是非常简单的虚拟版本也不起作用。我有模式（P => Q）和（不是 P => Q'）。我不知道为什么 Z3 给了我一个未知数。

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real))) )
  (=>
    (forall ((j Int)) (= (SameArray pattern (select list j)) false))
    (= (Match pattern list) (- 1))
  )
))

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real))) )
  (=>
    (not (forall ((j Int)) (= (SameArray pattern (select list j)) false)))
    (= (Match pattern list) 1)
  )
))
4

2 回答 2

0

我觉得您禁用了MBQI和AUTO_CONFIG，就像在您的代码变体中所做的那样。在那里，你会得到一个unknown用于第一个check-sat和一个unsat用于第二个。如果你评论两个set-options，你会得到satand unsat。

这unsat是预期的，因为push/pop范围内的断言与您的第一公理相矛盾。

关于unknownvssat我不得不推测一下。根据我的理解，MBQI它试图为所有未解释的符号找到一个解释，也就是说，它试图找到一个模型，使得给定的断言可以得到满足。

如果没有MBQI，Z3 依赖于 E 匹配，也就是说，它不会尝试为未解释的符号找到解释。Z3 确实试图找到一个矛盾，但在第一个点之前做出的断言check-sat并不相互矛盾。由于该问题不包含可推导的矛盾，而是 Z3 所知甚少的未解释符号，因此 Z3 所能报告的只有unsat.

于 2013-06-27T14:39:05.503 回答
0

问题是可以解决的。主要问题是该函数Match只是声明而未定义，Z3 在处理附加公理方面存在问题。虽然这对SameArray函数没有问题，但Match函数失败了。正确的定义如下：

(define-fun SameArray ((array1 (Array Int Real)) (array2 (Array Int Real))) Bool
  (ite (forall ((i Int)) (= (select array1 i) (select array2 i) )) true false)
)


(define-fun Match ((pattern (Array Int Real)) (list (Array Int (Array Int Real))) ) Int
  (ite 
    (exists ((index Int))
      (and
        (= (SameArray pattern (select list index)) true)
        (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index)))
      )
    )
    1 0)
)
于 2013-07-10T14:53:24.373 回答