3

我对使用通用量词和 declare-const 而不使用 forall 感到有些困惑

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((x Int)) (>= (f x x) (+ x a))))

我可以这样写：

(declare-const x Int)
(assert  (>= (f x x) (+ x a))))

在这两种情况下，Z3 将探索 Int 类型的所有可能值。那么有什么区别呢？我真的可以使用 declare-const 来消除 forall 量词吗？

4

2 回答 2

5

您可以exists使用declare-const. 也许这就是你困惑的根源？以下两个是等价的：

    (assert (exists ((x Int)) (> x 0)))
    (check-sat)

和

   (declare-fun x () Int)
   (assert (> x 0))
   (check-sat)

请注意，这仅适用于顶级存在量词。如果您对共相 ( forall) 和存在量 ( exists) 进行了嵌套量化，那么您可以进行 skolemization 以将存在量浮动到顶层。从逻辑的角度来看，这个过程涉及更多，但相当简单。

没有以这种方式将全称量词浮动到顶层的通用方法，至少在 SMT-Lib 所体现的经典逻辑中没有。

于 2012-11-06T17:53:41.097 回答
5

不，说法不一样。Z3 中的常量是 nullary (0 arity) 函数，所以(declare-const a Int)只是 的语法糖(declare-fun a () Int)，所以这两个语句是相同的。你的第二个语句(assert (>= (f x x) (+ x a))))隐含地断言 x 的存在，而不是你第一个语句中的所有 x (assert (forall ((x Int)) (>= (f x x) (+ x a))))。为了清楚起见，请注意在您的第二个语句中，只有一个 x 的赋值需要满足断言，而不是所有可能的赋值（还要注意函数 f 的区别，并参见这个 Z3@rise 脚本：http://rise4fun .com/Z3/4cif）。

这是该脚本的文本：

(set-option :mbqi true)
(declare-fun f (Int Int) Int)
(declare-const a Int)
(declare-fun af () Int)
(declare-const b Int)
(declare-fun bf () Int)

(push)
(declare-const x Int)
(assert  (>= (f x x) (+ x a)))
(check-sat) ; note the explicit model value for x: this only checks a single value of x, not all of them
(get-model)
(pop)

(push)
(assert (forall ((x Int)) (>= (f x x) (+ x a))))
(check-sat)
(get-model) ; no model for x since any model must satisfy assertion
(pop)

此外，这是 Z3 SMT 指南中的一个示例（“未解释的函数和常量”部分下的http://rise4fun.com/z3/tutorial/guide ）：

(declare-fun f (Int) Int)
(declare-fun a () Int) ; a is a constant
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
(assert (> a 20))
(assert (> b a))
(assert (= (f 10) 1))
(check-sat)
(get-model)
于 2012-11-06T02:29:57.587 回答