排序参数包装函数

Question

假设使用几个内置和用户定义的 Z3 排序，例如Int，Bool，S1，S2，...，有没有办法编写一个通用的排序包装和展开函数，从排序 A 转换到排序 B 并返回？例如

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(WRAP[S1] b) ; Expression is of sort S1
(WRAP[S1] c) ; Expression is of sort S1
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int

我目前手动覆盖每个案例，例如

(declare-fun $boolToInt (Bool) Int)
(declare-fun $intToBool (Int) Bool)

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

(assert (forall ((x Bool))
  (= x ($intToBool($boolToInt x)))))

这样的包装可以从一组给定的排序中自动创建，但我更喜欢可能的通用解决方案。

Answer 1

您可以使用数据类型来编码“联合类型”。 这是一个例子：

(declare-sort S1)
(declare-sort S2)

(declare-datatypes () ((S1-S2-Int (WRAP-S1 (S1-Value S1))
                                  (WRAP-S2 (S2-Value S2))
                                  (WRAP-Int (Int-Value Int)))))

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(simplify (WRAP-S1 a))
(simplify (= (WRAP-S1 a) (WRAP-Int 10)))
(simplify (S1-Value (WRAP-S1 a)))
(simplify (is-WRAP-S2 (WRAP-S1 a)))
(simplify (is-WRAP-S1 (WRAP-S1 a)))
(simplify (is-WRAP-Int (WRAP-Int c)))
(simplify (S1-Value (WRAP-S2 b)))

您可以在Z3 guide 中找到有关数据类型的更多信息。数据类型S1-S2-Int 具有三个构造函数：WRAP-S1、WRAP-S2 和WRAP-Int。 Z3 自动生成识别器谓词：is-WRAP-S1、is-WRAP-S2 和 is-WRAP-Int。访问器S1-Value、S2-Value 和Int-Value 用于“解构”S1-S2-Int 值。例如，对于所有a、(S1-Value (WRAP-S1 a)) = a。 (S1-Value (WRAP-S2 b)) 的值未指定。在这种情况下，Z3 将S1-Value 视为未解释的函数。

顺便说一句，公理

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

等价于假。它本质上是试图将整数注入布尔值。