在 Z3 中定义枚举类型的函数

Question

我有一个枚举类型 BoolT 包含 Bool 和 Bot

(declare-datatypes () ((BoolT Bool Bot)))

我想定义一个相等函数 eq，如果其中一个参数是 BotBoolT 返回 Bot /em>，否则两个 Bool 参数相等。但是，我无法定义布尔值之间的实际比较。直到现在我得到了这个功能

(define-fun eq ((x1 BoolT) (x2 BoolT)) BoolT
    (ite (or (= x1 Bot) (= x2 Bot)) Bot Bool))

虽然我需要类似的东西

(define-fun eq ((x1 BoolT) (x2 BoolT)) BoolT
    (ite (or (= x1 Bot) (= x2 Bot)) Bot 
           (or (and (= x1 true)(= x2 true)) (and (= x1 false)(= x2 false)))
)

或至少是以下谓词的正确定义

(define-fun is-True ((x1 BoolT)) Bool 
     (ite (= x1 true) true false)
)

有没有办法对 eq 函数或 BoolT 上的前一个谓词进行建模？

Answer 1

您将需要 Z3 中的标记联合，类似于 ML 数据类型。您不能只取现有类型的并集并将其包含在数据类型声明中。 所以你需要写这样的东西：

   (declare-datatypes () ((BoolT True False Bot)))

或

   (declare-datatypes () ((BoolT (mkB (tf B)) Bot) (B True False)))

然后你可以写：

 (define-fun is-True1 ((x BoolT)) Bool 
    (= (mkB True) x))

或

 (define-fun is-True2 ((x BoolT)) Bool 
 (and (is-mkB x) (= True (tf x))))

和断言

 (declare-const a BoolT)
 (assert (is-True2 a))

声明（B真假） 自动声明谓词 is-True 和 is-False

 (declare-const b B)
 (assert (is-True b))