1

我尝试在 Z3 中使用数组并注意到我无法解释的奇怪行为。我首先定义了一些对(Array Int Object). (Array Int Real)后来我定义了一个不应该被其他函数混淆的类型的数组，因为它们有不同的类型。然后我开始向我的数组添加数字，一开始一切都很好，但是将第三个元素添加到我的数组让我的规范分解在一起。此外，如果我删除一个对所有事物都起作用的函数的公理，它会(Array Int Object)再次起作用。我不知道为什么会发生这种情况并希望有人对此有所了解。

; Declaration of concepts
(declare-datatypes () ((Object ObjectA ObjectB ObjectC)))

; Be aware that the following functions work on (Array Int Object) and we define an array of type (Array Int Real) later
(declare-fun Length ( (Array Int Object) ) Int)   ; The concrete length will be assert for each array of the type (Array Int Object)
(define-fun SameArray ( (array1 (Array Int Object)) (array2 (Array Int Object))) Bool
  (ite 
    (and
      (= (Length array1) (Length array2))
      (forall ((i Int)) (or (< i 0) (>= i (Length array1)) (= (select array1 i) (select array2 i) )) ) 
    )
    true
    false
  )
)

(declare-fun Match ((Array Int Object) (Array Int (Array Int Object))) Int) ; The concrete behavior for Match will be asserted for each necessary array.

; If the following axiom is deleted everything works fine
; Axioms: Equal arrays should behave equal for the Match function.
(assert (forall ( (array1 (Array Int Object)) (array2 (Array Int Object)) (list (Array Int (Array Int Object))))
  (ite
    (SameArray array1 array2)
    (= (Match array1 list) (Match array2 list))
    (not (= (Match array1 list) (Match array2 list)))
  )
))

(echo "General Definitions:")
(check-sat) ; Everything is OK here

(declare-const arr-Lookup-1 (Array Int Real))
(echo "Array Declaration:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 0 0.0) arr-Lookup-1))
(echo "Array1 Definition 1:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 1 100.0) arr-Lookup-1))
(echo "Array1 Definition 2:")
(check-sat) ; Everything is OK here

(assert (= (store arr-Lookup-1 2 1000.0) arr-Lookup-1))
(echo "Array1 Definition 3:")
(check-sat) ; This gives us an unknown 

(assert (= (store arr-Lookup-1 3 10000.0) arr-Lookup-1))
(echo "Array1 Definition 4:")
(check-sat)
4

0 回答 0