1

カスタム決定手順をZ3とインターフェースする方法について、NikolaiのZ3を使用した工学理論に関する記事を読んでいます。そこでは、AssertTheoryAxiom、NewAssignment、FinalCheckなどのいくつかのメソッドが言及されています。ただし、最新の（新しい？）Z3 API（http://research.microsoft.com/en-us/um/redmond/projects/z3/namespace_microsoft_1_1_z3.html ）でそれらを見つけることができませんでした。誰かが私に彼らまたは彼らの代替品がどこにあるか教えてもらえますか？2.関連するメモで、プローブや戦術などのインターフェイスにいくつかの新しい概念があります。これらはどこかで説明または説明されていますか？

4

1 に答える 1

1

カスタム決定手順のインターフェースは現在非推奨です。これらは、古いソルバー API で引き続き使用できます。詳細については、次の投稿を参照してください。

非推奨の API の完全なリストは次のとおりです。タクティクスとプローブについては、この記事と、それに関する Z3 チュートリアル ( PythonおよびSMT 2.0 ) を参照してください。

于 2012-12-27T03:30:39.673 に答える