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

Question

我有一些混淆使用通用量词和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量词吗？

Answer 1

不,这些陈述是不同的.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,"Uninterpreted functions and constants"部分):

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

Answer 2

您可以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 所体现的经典逻辑中没有。