有没有办法使用Z3来获得有关序列和地图的约束的模型？ [英] Is there a way to use Z3 to get models for constraints involving sequences and maps?

问题描述

前一段时间，我问我如何使用Z3来获取有关集合约束的模型（有没有办法使用Z3来获取有关集合的约束的模型？对于这个扩展的数组理论在我的情况下工作得很好。

现在我已经有序列的同样的问题（操作长度，成员资格，（内部）相等切片）和地图。即公理化导致与集相同的问题。我一直在考虑使用扩展阵列理论编码序列和地图，但是我还没有想出一个很好的方式来实现。

有没有人想知道如何编码序列和地图以获得准确的模型？

解决方案

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））
 -sat）
（get-model）
  

对于序列，我们可以使用量词。 Z3对于许多可分解的碎片是完整的。
大部分都在 Z3教程中描述。 这里是可能的编码。

  ;;在这个例子中，我们编码了T. 
 ;;的序列。让我们让T == Int 
（define-sort T（）Int）
 
 ;;我们将一个序列作为一个对：function + length 
（declare-fun S1-data（Int）T）
（declare-const S1-len Int）
 
 -fun S2-data（Int）T）
（declare-const S2-len Int）
 
（声明乐趣S3数据（Int）T）
（declare- const S3-len Int）
 
 ;;这种编码有一个限制，我们不能有序列序列;也没有序列作为函数的参数。 
 
 ;;我们如何断言序列S1和S2是相等的。 
（push）
（assert（= S1-len S2-len））
（assert（for（（int Int））（=>（和（< = 0 i） （< i S1-len））（=（S1-data i）（S2-data i）））））
 ;;为了使该例更有趣，让我们假设S1-len> 0 
（assert（> S1-len 0））
（check-sat）
（get-model）
（pop）
 
; ;以下是我们如何说序列S3是序列S1和S2的级联。 
（推）
（assert（= S3-len（+ S1-len S2-len）））
（assert（for（（int Int））（=> < = 0 i）（< i S1-len））（=（S3-数据i）（S1数据i）））））
（assert（for（i Int））（=& ;（和（< = 0 i）（< i S2-len））（=（S3-data（+ i S1-len））（S2-数据i））））
;让我们断言S1-len和S2-len> 1 
（assert（> S1-len 1））
（assert（> S2-len 1））
 ;;我们也断言S3（0）！= S3（1）
（assert（not（=（S3-data 0）（S3-data 1））））
（check-sat）
（get-model）
（pop）
 
 ;;这是我们如何编码序列S2是具有一个额外元素的序列S1 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）） （=<（< = 0 i）（< i S1-len））（=（S2-数据i）（S1-数据i）））））
 ;;让我们也断言S1-len> 1 
（assert（&S1。1 len 1））
（check-sat）
（get-model）
（pop）
  

Some time ago I asked how I could use Z3 to get models for constraints involving sets (Is there a way to use Z3 to get models for constraints involving sets?). For this the extended array theory works well in my case.

Now I have got the same issue with sequences (with operations length, membership, (in-)equality, perhaps slicing) and maps. I.e. axiomatization leads to the same problem as for sets. I have been thinking of encoding sequences and maps using the extended array theory as well but I have not yet been able to come up with a good way to do this.

Does anyone have an idea on how sequences and maps could be encoded to get accurate models?

解决方案

In Z3, arrays are essentially maps. Here is an example on how to create an "array" from list of integers to integers.

(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)

For sequences, we can encode them using quantifiers. Z3 is complete for many decidable fragments. Most of them are described in the Z3 tutorial. Here is a possible encoding.

;; 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)

这篇关于有没有办法使用Z3来获得有关序列和地图的约束的模型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！