3

我已经定义了自己的布尔值，称为booleanSMT2，以及boolean_and它们的 AND 函数。我的猜想是 AND 是可交换的：

(declare-sort boolean)
(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-const boolean_false boolean)
(declare-const boolean_true boolean)
(declare-fun boolean_and (boolean boolean) boolean)

;; axiomatize booleans: false /= true and every bool is true or false
(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

(assert (not (= boolean_false boolean_true)))

;; definition of AND
(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

;; try to prove that AND is commutative
(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

然而，z3 在一段时间后报告了这个问题的未知数，尽管我认为它应该能够对 skolemised 变量sk_x和sk_y.

奇怪的是，如果我删除我的布尔公理化并将其替换为 declare-datatypes，z3 将报告unsat：

(declare-datatypes () ((boolean (boolean_true) (boolean_false))))

(declare-const sk_x boolean)
(declare-const sk_y boolean)
(declare-fun boolean_and (boolean boolean) boolean)

(assert (forall ((a boolean)) (= (boolean_and boolean_false a) boolean_false)))
(assert (forall ((a boolean)) (= (boolean_and boolean_true a) a)))

(assert (not (= (boolean_and sk_x sk_y)
                (boolean_and sk_y sk_x))))

(check-sat)

我究竟做错了什么？如何使用我的公理化让 z3 进行案例拆分？

4

1 回答 1

3

你没有做错任何事。官方版本（v4.3.1）可能会因包含基数约束的问题而失败，例如

(assert (forall ((x boolean)) (or (= x boolean_false)
                                  (= x boolean_true))))

这个约束断言未解释的排序boolean最多有两个元素。我解决了这个问题。该修复程序已在unstable分支中可用。 以下是有关如何编译unstable分支的一些说明。明天，夜间版本也将包含此修复程序。

于 2013-03-18T15:32:41.753 回答