1

あるルールをシミュレートするある種のアプリケーションを書いています。Z3py の不動点が助けになることがわかりました。私のアプリの概要は次のようになります: (fp = Fixedpoint())

  1. a, b, c = Ints('ab c') などの整数変数を宣言し、固定小数点 - fp.(a, b, c) に登録します。

  2. いくつかの変数の性質 (事実) に従って、他のいくつかの変数を増減します。例: (a>0 かつ b>0) の場合、c=c+1

  3. ターゲット変数が何らかの条件を満たしているかどうかを照会します。たとえば、query(target>0)

2 を指定するルールの使い方がわかりません。

4

1 に答える 1

1

あなたが概説した例を取り上げ、例を作成しました：

これが役立つことを願っています。

クエリに到達できないため、Z3 は UNSAT を出力します。次に、クエリに到達できないことを証明する不変式を表示します。

さらに詳細に

3 つの引数を持つプロパティを宣言するには、次のようにします。

P = Function('P', IntSort(), IntSort(), IntSort(), BoolSort())

これを固定小数点エンジンに登録するには、次のようにします。

fp.register_relation(P)

念頭に置いているルールを追加します。

fp.rule(P(-1,1,-10))
fp.rule(P(a,b,c+1), [a > 0, b > 0, P(a,b,c)])
fp.rule(P(a+1,b,c-1), [a <= 0, b < 0, P(a,b,c)])

最初のルールは、プロパティが最初に保持するものについて何かを述べています。2 番目のルールは、a > 0、b > 0 の場合に c をインクリメントできることを示しています。

最後に、到達可能なプロパティがあるかどうかを尋ねます。

print fp.query(P(a,b,c),c > 0 )
于 2013-02-27T17:19:26.570 に答える