带 Z3 求解器的三值布尔逻辑

Question

我一直在尝试使用 Z3 SMT Solver 定义一个三值命题逻辑并对其进行推理。更准确地说，我定义了一个具有三个值的排序布尔值：TRUE、FALSE 和 NULL，并带有一些断言。

(declare-sort Boolean 0)       ;I declare a sort Boolean
(declare-const TRUE Boolean)   ;I define three constants
(declare-const TRUE Boolean)
(declare-const FALSE Boolean)
(declare-const NULL Boolean)

(assert (distinct TRUE FALSE)) ;I define the meaning of these constants
(assert (distinct TRUE NULL))
(assert (distinct FALSE NULL))

(assert (forall ((b Boolean))
    (or (= b TRUE)
        (= b FALSE)
        (= b NULL))))

接下来，假设我在这个逻辑下定义一个 >= 整数运算符的语义，假设整数可以为 NULL。

(declare-const nullInt Int)
(declare-fun >=_B (Int Int) Boolean)

(assert (forall ((i1 Int) (i2 Int))
    (= (= TRUE (>=_B i1 i2))
       (and (distinct i1 nullInt)
            (distinct i2 nullInt)
            (>= i1 i2)))))

(assert (forall ((i1 Int) (i2 Int))
    (= (= FALSE (>=_B i1 i2))
       (and (distinct i1 nullInt)
            (distinct i2 nullInt)
            (not (>= i1 i2))))))

(assert (forall ((i Int))
    (= NULL (>=_B i nullInt))))

(assert (forall ((i Int))
    (= NULL (>=_B nullInt i))))

最后，根据上述定义，我在我的断言中使用了 >=_B 函数，但不断出现意外的 UNSAT 或未知。我想知道是什么让这个理论落入了不可判定的领域。是因为我做的布尔排序吗？还是因为我在 Int 的无限集上进行量化的断言？

Answer 1

我认为您使用量词和未解释的排序使建模复杂化。简单地让你的布尔值成为枚举并相应地定义你的谓词：

(declare-datatype Boolean ((TRUE) (FALSE) (NULL)))

(declare-const nullInt Int)

(define-fun >=_B ((i1 Int) (i2 Int)) Boolean
    (ite (or (= i1 nullInt) (= i2 nullInt)) NULL (ite (>= i1 i2) TRUE FALSE)))

(check-sat)
(get-model)

这会产生：

sat
(
  (define-fun nullInt () Int
    0)
)

任意选择 nullInt 作为 0。现在您可以在此基础上构建其他操作，并对您想要的三值逻辑的任何方面进行建模。

两个注意事项：

我写了我能想到的 >=_B 最“明显”的定义，不过您应该检查以确保这符合您的直觉。
将 nullInt 作为未解释的常量很奇怪。您真正想要的可能是“扩展”整数。即，整数和一个新值 null-int。但是，您建模的内容不会那样做。但是你可以用 declare-datatype 做同样的事情并创建扩展整数的类型并相应地定义 >=_B 。我会使用以下形式的类型：

(declare-datatype NullableInt ((NullInt) (RegInt (getRegInt Int))))

然后定义您对该类型的所有操作。当然，这更麻烦，因为您还必须提升所有算术运算（即 +、-、* 等）。

最后说明：虽然 SMTLib lingua-franca 适用于 SMT 求解器，但它并不是最人性化的 readable/writable。如果您正在试验，我建议您使用 higher-level 界面，例如来自 Python/Haskell 等的界面，它可以消除大部分噪音。

带 Z3 求解器的三值布尔逻辑

A three-valued boolean logic with Z3 solver

z3

smt

three-valued-logic