前一段时间，我问我如何使用Z3获得的模型涉及约束集（ 有没有办法使用Z3获得的模型涉及约束集的方法吗？ ）。 对于这个扩展的阵列理论效果很好在我的情况。
现在，我已经得到了与序列相同的问题（与运营长，会员，（活）平等，也许切片）和地图。 即公理化导致了同样的问题，作为集。 我一直在想编码使用扩展的阵列理论以及序列和地图，但我还没有能够拿出一个好的办法做到这一点。
有没有人对序列和地图如何进行编码以获得精确的模型的想法？
Answer 1:
在Z3，数组实质上映射。 下面是关于如何创建一个从整数到整数的列表“阵列”的一个例子。
(declare-const a (Array (List Int) Int))
(declare-const l1 (List Int))
(declare-const l2 (List Int))
(assert (= (select a l1) 0))
(assert (= (select a l2) 0))
(check-sat)
(get-model)
对于序列，我们可以使用量词进行编码。 Z3是完成了许多可判定的片段。 他们大多是在描述Z3教程 。 这里是一个可能的编码。
;; In this example, we are encoding sequences of T.
;; Let us make T == Int
(define-sort T () Int)
;; We represent a sequence as a pair: function + length
(declare-fun S1-data (Int) T)
(declare-const S1-len Int)
(declare-fun S2-data (Int) T)
(declare-const S2-len Int)
(declare-fun S3-data (Int) T)
(declare-const S3-len Int)
;; This encoding has one limitation, we can't have sequences of sequences; nor have sequences as arguments of functions.
;; Here is how we assert that the sequences S1 and S2 are equal.
(push)
(assert (= S1-len S2-len))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S1-data i) (S2-data i)))))
;; To make the example more interesting, let us assume S1-len > 0
(assert (> S1-len 0))
(check-sat)
(get-model)
(pop)
;; Here is how we say that sequence S3 is the concatenation of sequences S1 and S2.
(push)
(assert (= S3-len (+ S1-len S2-len)))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S3-data i) (S1-data i)))))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S2-len)) (= (S3-data (+ i S1-len)) (S2-data i)))))
;; let us assert that S1-len and S2-len > 1
(assert (> S1-len 1))
(assert (> S2-len 1))
;; let us also assert that S3(0) != S3(1)
(assert (not (= (S3-data 0) (S3-data 1))))
(check-sat)
(get-model)
(pop)
;; Here is how we encode that sequence S2 is sequence S1 with one extra element a
(push)
(declare-const a T)
(assert (> a 10))
(assert (= S2-len (+ 1 S1-len)))
(assert (= (S2-data S1-len) a))
(assert (forall ((i Int)) (=> (and (<= 0 i) (< i S1-len)) (= (S2-data i) (S1-data i)))))
;; let us also assert that S1-len > 1
(assert (> S1-len 1))
(check-sat)
(get-model)
(pop)
文章来源: Is there a way to use Z3 to get models for constraints involving sequences and maps?
