z3 - 如何在Z3中编写代码

我正在尝试在Z3中编码一个非常简单的问题，但是我感到困惑，而且我不知道如何正确解决它。

所以我有一个包含这些元素的数组(Python语法样式代码):

array = [0, -1, 1, 8, 43]

而且我可以使用索引访问此数组:

x = array[index]

最后，我想问z3我需要使用什么索引来获取元素8，在我的示例中，解决方案是index = 3(从0开始)。

我试图在Z3中编码此问题，我写了以下几行:

(declare-const x Int)
(declare-const index Int)

(assert (= x
           (ite (= index 0)
                0
           (ite (= index 1)
                -1
           (ite (= index 2)
                1
           (ite (= index 3)
                8
           (ite (= index 4)
                43
           999999)))))))
(assert (= x 8))
(check-sat)
(get-model)

它正在工作，我有以下解决方案:

sat
(model
  (define-fun index () Int
    3)
  (define-fun x () Int
    8)
)

但是我不喜欢最后一个，即999999。我需要使用一个魔术数字来知道何时找不到该值。我试图查看是否存在没有else的“it”构造，或者是否有NULL / None / UNSAT或任何特殊值都没有此问题。

解决此问题的正确方法是什么？

感谢您的帮助!

最佳答案

对于解决此问题的“正确”方法，我一无所知，因为首先应该定义“正确”。

但是，可以通过多种方式将其编码为smt2公式。

示例0。

通过简单地迫使索引落在域[0，4]内，就可以使ite执行所需的操作而无需任何幻数。

(declare-const x Int)
(declare-const index Int)

(assert (= x
           (ite (= index 0)
                0
           (ite (= index 1)
                -1
           (ite (= index 2)
                1
           (ite (= index 3)
                8
           43))))))

(assert (and (<= 0 index) (<= index 4)))

(assert (= x 8))
(check-sat)
(get-model)

这将返回您所需的模型:

~$ z3 example_00.smt2
sat
(model
  (define-fun index () Int
    3)
  (define-fun x () Int
    8)
)

示例1.

(declare-const x Int)
(declare-const index Int)

(assert (ite (= index 0) (= x 0) true))
(assert (ite (= index 1) (= x (- 1)) true))
(assert (ite (= index 2) (= x 1) true))
(assert (ite (= index 3) (= x 8) true))
(assert (ite (= index 4) (= x 43) true))

(assert (and (<= 0 index) (<= index 4)))

(assert (= x 8))
(check-sat)
(get-model)

这将返回您所需的模型:

~$ z3 example_01.smt2
sat
(model
  (define-fun index () Int
    3)
  (define-fun x () Int
    8)
)

示例2.

(declare-const x Int)
(declare-const index Int)

(assert (or (not (= index 0)) (= x 0)))      ;; (= index 0) -> (= x 0)
(assert (or (not (= index 1)) (= x (- 1))))
(assert (or (not (= index 2)) (= x 1)))
(assert (or (not (= index 3)) (= x 8)))
(assert (or (not (= index 4)) (= x 43)))

(assert (and (<= 0 index) (<= index 4)))

(assert (= x 8))
(check-sat)
(get-model)

这将返回您所需的模型:

~$ z3 example_02.smt2
sat
(model
  (define-fun index () Int
    3)
  (define-fun x () Int
    8)
)

示例3.

使用阵列理论

(declare-fun x () Int)
(declare-fun index () Int)
(declare-const ar (Array Int Int))

  ; array's locations initialization
(assert (= (store ar 0 0)     ar))
(assert (= (store ar 1 (- 1)) ar))
(assert (= (store ar 2 1)     ar))
(assert (= (store ar 3 8)     ar))
(assert (= (store ar 4 43)    ar))

  ; x = ar[index]
(assert (= (select ar index) x))

  ; bound index to fall within specified locations
(assert (and (<= 0 index) (<= index 4)))

  ; x = 8
(assert (= x 8))

  ; check
(check-sat)
(get-model)

这将返回您所需的模型:

~$ z3 example_03.smt2
sat
(model
  (define-fun x () Int
    8)
  (define-fun ar () (Array Int Int)
    (_ as-array k!0))
  (define-fun index () Int
    3)
  (define-fun k!0 ((x!0 Int)) Int
    (ite (= x!0 2) 1
    (ite (= x!0 3) 8
    (ite (= x!0 1) (- 1)
    (ite (= x!0 0) 0
    (ite (= x!0 4) 43
      5))))))
)

其他示例也是可能的。

理想情况下，应该选择z3在求解公式中具有最佳性能的编码。在这方面，我无能为力，因为我通常会与其他SMT求解器打交道。

通常，使用更复杂的理论(例如数组理论)会导致运行时执行更昂贵的例程，因此人们可能会认为最好避免这种情况。但是，根据我的经验，这不是一般的经验法则，因为即使是很小的编码变化也会导致明显的性能差异，非常差的或幼稚的编码可能会产生非常差的效果。因此，始终最好对各种候选编码执行广泛的基准测试。