如何在 Z3 中编码

Question

我正在尝试在 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 或任何特殊值都没有这个问题。

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

感谢您的帮助！

Answer 1

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

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

---

示例 0。

通过简单地强制 index 进入域 [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 求解器打交道。

一般来说，使用更复杂的理论（例如数组理论）会导致运行时执行更昂贵的例程，因此人们可能认为最好避免它。但是，我会说，根据我的经验，这不是一般的经验法则，因为即使编码的微小变化也会导致显着的性能差异并且非常差或naive 编码可能会执行得非常糟糕。因此，最好对各种候选编码执行广泛的基准测试。