SMTLIB中如何定义接收参数化Pair类型的函数

首先明确：SMTLIB支持声明接收参数化类型的函数，既可以声明处理固定类型实例化参数的函数，也可以声明通用的参数化泛型函数。

你给出的参数化Pair类型声明如下：

(declare-datatypes ((Pair 2)) (
  (par (X Y) ((pair (first X) (second Y))))
))

两种声明场景示例 #

1. 接收固定类型实例化Pair的函数 #

如果你的函数只需要处理特定类型的Pair，比如两个元素都是Int的Pair，直接在参数位填入实例化后的类型即可，示例如下：

; 声明一个接收(Int, Int)类型Pair，返回两数之和的函数
(define-fun sumPair ((p (Pair Int Int))) Int
  (+ (first p) (second p))
)

2. 通用参数化函数（支持任意类型的Pair） #

如果需要声明适配所有类型Pair的泛型函数，需要用par关键字声明函数的类型参数，示例如下：

; 声明一个交换Pair两个元素位置的泛型函数
(define-fun swap ((X Type) (Y Type) (p (Pair X Y))) (Pair Y X)
  (pair (second p) (first p))
)

; 调用示例：交换元素类型为Int和String的Pair
(swap Int String (pair 1 "测试内容"))

注：以上语法适配SMTLIB 2.6及以上版本，Z3、CVC5等主流SMT求解器均支持该特性。

内容的提问来源于stack exchange，提问作者JRR