z3 - 我可以使用 declare-const 来消除 forall 通用量词吗？

Question

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

(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))))

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

Answer 1

不，陈述不同。 Z3 中的常量是 nullary (0 arity) 函数，所以 (declare-const a Int) 只是 (declare-fun a () Int) 的语法糖，所以这些两个陈述是相同的。您的第二个语句 (assert (>= (f x x) (+ x a)))) 隐式断言 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)