3

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

Z3を使用すると、この2つのケースでInt型のすべての可能な値が調査されます。では、違いは何ですか？本当にdeclare-constを使用して、forall数量詞を削除できますか？

4

2 に答える 2

5

いいえ、ステートメントは異なります。Z3の定数はnullary（0 arity）関数であるため、(declare-const a Int)の構文上の砂糖であるため(declare-fun a () Int)、これら2つのステートメントは同一です。2番目のステートメント(assert (>= (f x x) (+ x a))))は、最初のステートメントのようにすべてのxに対してではなく、xの存在を暗黙的に表明します(assert (forall ((x Int)) (>= (f x x) (+ x a))))。明確にするために、2番目のステートメントでは、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 に答える
5

を使用してトップレベルexistsを削除できdeclare-constます。多分これはあなたの混乱の原因ですか？次の2つは同等です。

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

と

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

これは、最上位の存在記号にのみ適用されることに注意してください。ユニバーサル（forall）と実存（）の両方の数量化をネストしている場合existsは、スコーレム化を実行して実存をトップレベルにフロートさせることができます。このプロセスはより複雑ですが、論理的な観点からはかなり単純です。

少なくともSMT-Libによって具体化される古典論理では、この方法で全称記号をトップレベルに浮動させる一般的な方法はありません。

于 2012-11-06T17:53:41.097 に答える