时间戳

首页 > 解决方案 > 什么是地图[f]

z3 - 什么是地图[f]

问题描述

假设我有一个排序 T 并且我声明了一个由 T 索引的数组，它的映射类型是什么？

例如

(declare-datatypes ()
  ((T ....))) ; some index, may be finite or infinite (as in Int)
(declare-const a (Array T Int))
(declare-const b (Array Int Int))
(define-fun foo ((x Int)) Int)
(define-fun bar ((y Int)) Bool)

foo 上的映射是什么？和 b 上的那种映射 foo？有没有办法弄乱索引类型并从由 T 索引的数组中获取由另一种排序索引的数组，例如 Int？

标签： z3smt

解决方案

通常的排序匹配规则适用。也就是说，对于数组上map的函数f : A -> B，数组必须有它的范围类型A，并且它将把它变成 a B，保留其域的类型。

关于您的示例：无论您T是什么，如果您 map ，您将只是Array T Int作为最终排序，如果您 map foo，Array T Bool则作为结果bar。以下脚本类型检查没有任何问题：

(declare-datatypes ((T 0)) ((i Int)))
(declare-const a (Array T Int))
(declare-const b (Array Int Int))
(declare-fun foo (Int) Int)
(declare-fun bar (Int) Bool)

(define-fun e1 () (Array T  Int)   ((_ map foo) a))
(define-fun e2 () (Array T  Bool)  ((_ map bar) a))
(define-fun e3 () (Array Int Int)  ((_ map foo) b))
(define-fun e4 () (Array Int Bool) ((_ map bar) b))

请注意，您不能通过index将函数映射到数组来更改域的类型（我认为这是您的意思）。它只会更改范围类型。

推荐阅读