如何从 Z3 中的 Seq 类型中提取元素作为基本类型？答案

【问题标题】：How do you extract an element as the base type from a Seq type in Z3?如何从 Z3 中的 Seq 类型中提取元素作为基本类型？
【发布时间】：2017-10-11 20:28:06
【问题描述】：

如何将序列中的元素提取到基本类型，以便以下工作？

(define-sort ISeq () (Seq Int))
(define-const x ISeq (seq.unit 5))
(define-const y ISeq (seq.unit 6))
(assert (>= (seq.at x 0) (seq.at y 0)))

【问题讨论】：

标签： z3

【解决方案1】：

您正在寻找nth。这是一个简单的例子：

(define-sort ISeq () (Seq Int))
(declare-const x ISeq)
(declare-const y ISeq)
(assert (= (seq.len x) 4))
(assert (= (seq.len y) 3))
(assert (< (seq.nth x 3) (seq.nth y 1)))
(check-sat)
(get-value (x y))

z3 会立即给出正确答案 (1237 > 1236)：

sat
((x (seq.++ (seq.unit 6)
        (seq.++ (seq.unit 7) (seq.++ (seq.unit 8) (seq.unit 1236)))))
 (y (seq.++ (seq.unit 9) (seq.++ (seq.unit 1237) (seq.unit 12)))))

【讨论】：

【解决方案2】：

在实现合适的功能（或向我们揭示它的存在）之前，您可以使用以下解决方法：

(define-sort ISeq () (Seq Int))
(define-const x ISeq (seq.unit 5))
(define-const y ISeq (seq.unit 6))

(declare-const e1 Int)
(declare-const e2 Int)

(push)
  (assert (= (seq.unit e1) (seq.at x 0)))
  (assert (= (seq.unit e2) (seq.at y 0)))

  (assert (not (>= e2 e1)))
  (check-sat)
(pop)

(push) ;; or alternatively
  (assert (not
    (implies
      (and
        (= (seq.unit e1) (seq.at x 0))
        (= (seq.unit e2) (seq.at y 0)))
      (>= e2 e1))))
  (check-sat)
(pop)

【讨论】：

【解决方案3】：

在 Z3 问题跟踪器中查看相关讨论：https://github.com/Z3Prover/z3/issues/1302

似乎确实有一种解决方法，但由于量词，它不太可能为您提供有效的方法。同时，像 Malte 这样的显式编码可能是最实用的方法。

【讨论】：