1

假设使用几个内置的和用户定义的 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)))))

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

4

1 回答 1

3

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

(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 指南中找到有关数据类型的更多信息。该数据类型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)))))

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

于 2012-03-12T14:55:03.760 回答