5

基本上，我想要求 Z3 给我一个值大于 10 的任意整数。所以我写了以下语句：

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

如何将此量词应用于我的模型？我知道你可以写 (assert (> x 10)) 来实现这一点。但我的意思是我的模型中需要一个量词，所以每次我声明一个整数常量，其值保证超过 10。所以我不必为我的每个整数常量插入语句 (assert (> x 10))宣布。

4

1 回答 1

5

当您使用 时(assert (forall ((i Int)) (> i 10)))，i是一个有界变量，量化公式等价于一个真值，false在这种情况下就是这样。

我认为您想使用量词定义宏：

(declare-fun greaterThan10 (Int) Bool)
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10))))

您可以使用它们来避免代码重复：

(declare-const x (Int))
(declare-const y (Int))
(assert (greaterThan10 x))
(assert (greaterThan10 y))
(check-sat)

当您使用 Z3 API 时，它本质上是使用未解释函数定义宏的方法。请注意，您必须设置(set-option :macro-finder true)以便 Z3 用这些函数的主体替换通用量词。

但是，如果您使用的是文本界面，则define-funSMT-LIB v2 中的宏是一种更简单的方法来执行您想要的操作：

(define-fun greaterThan10 ((i Int)) Bool
  (> i 10))
于 2012-02-16T16:23:32.083 回答