1

Z3 を使用して、配列プロパティ フラグメント内の式の充足可能性を確認しています。Z3 が返す配列変数のモデルは通常、他の if 式や if-then-else の場合分けなどを使用して表現されます。 Z3 が出力するモデルを何らかの方法で解析し、入力 SMT-LIB 式を満たす配列を作成したい、明示的に。

たとえば、Z3 が次の形式に出力するモデルを常に単純化できるようにしたいと考えています。

A -> {
  1 -> 3
  2 -> 4
  else -> 6
}

モデルを (C API を使用して) トラバースし、モデルを表す明示的な配列を作成する簡単な方法はありますか?

4

1 に答える 1

0

残念ながら、あなたのメッセージで説明されている出力形式は、配列プロパティ フラグメント内のすべての充足可能な式のモデルを説明するのに十分な表現力を備えていません。たとえば、次の簡単な例を考えてみましょう。

(declare-fun f (Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (f i) (f j)))))
(assert (< (f a) (f b)))

(check-sat)
(get-model)

数式fは非減少で、2 つのポイントaとbstがありf(a) < f(b)ます。どのモデルでも、すべての値i <= a、f(i) <= f(a)、およびすべての値j >= bに対してそれが必要f(b) <= f(j)です。あれは、

f(i) <= f(a) < f(b) <= f(j).

シングルelseでは動作しません。Z3 は、f本質的に「ステップ関数」であるという解釈を生成します。ここで上記の例を試すことができます。

于 2013-07-09T00:50:16.710 に答える