1

Z3 apiでは、FuncDeclにDeclKind（）があり、それが書き換えルールであるかどうかを示します。しかし、Z3 Java APIで書き換えルールを作成するにはどうすればよいですか？

4

1 に答える 1

1

あなたの質問を正しく理解できたかどうかわかりません。のことZ3_OP_PR_REWRITEですか？その場合、これは Z3 証明の書き換え規則証明ステップに注釈を付けるために使用される宣言の種類です。これは、この記事(セクション 3.2)で説明されている書き換え手順に対応しています。この宣言の種類をユーザー定義の書き換え規則と混同しないでください。

于 2013-03-06T01:28:31.267 に答える