z3 - 如何在 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)
)

但我不喜欢最后一个 else，即 999999。我需要使用魔数(Magic Number)来知道何时找不到该值。我试着看看是否有一个没有 else 的“它”结构，或者 NULL/None/UNSAT 或任何特殊值没有这个问题。

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

谢谢你的帮助!

Answer 1

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

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

---

示例 0.

通过简单地强制 index 落在域 [0, 4] 内，您可以让 ite 做您想要的不需要任何魔数(Magic Number)。

(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 求解器。

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