1

我一直在尝试使用 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 的无限集上量化的断言？

4

1 回答 1

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。现在，您可以在此基础上构建其他操作，并对您想要的 3 值逻辑的任何方面进行建模。

两个注意事项：

  • 我已经写了我能想到的最“明显”的定义>=_B，尽管你应该检查以确保这符合你的直觉。

  • nullInt有一个未解释的常数很奇怪。您真正想要的可能是“扩展”整数。即，整数和新值null-int。但是，您建模的内容并没有做到这一点。但是您可以使用 a 做同样的技巧，declare-datatype并制作扩展整数的类型并>=_B相应地定义。我会使用一种形式：

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

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

最后说明：虽然 SMTLib 是 SMT 求解器的通用语言，但它并不是最人性化的可读/可写。如果您正在尝试，我建议使用更高级别的接口，例如 Python/Haskell 等中的接口，这样可以消除大部分噪音。

于 2022-01-25T16:25:01.850 回答