Z3 の python API を使用して、ある種のインクリメンタル ソリューションを実行しています。コマンドを使用して、各ステップで満たされないかどうかをチェックしながら、繰り返しソルバーに制約をプッシュしますsolver.push()。Z3 が以前の制約から学習した補題を使用するのか、それとも新しく追加された制約で解くときに以前に得られた満足のいく解を使用するのかを理解したいと思います。私は決してsolver.pop()コマンドを使用しません。以前の反復で行われた作業がどのように使用されているかについての詳細はどこで入手できますか?
3011 次
1 に答える
7
Z3 には複数のソルバーがありますが、インクリメンタル ソルバーと以前の呼び出しからの作業の再利用を実際にサポートしているのはそのうちの 1 つだけです。デフォルトでは、Z3 は を実行するたびに自動的にインクリメンタル ソルバーに切り替わりますsolver.push()。このソルバーは、以前に学習した句も再利用します。a を実行すると、学習した節は削除さsolver.pop()れます。pushZ3 は、およびに基づいていないインクリメンタル ソルビングの別のメカニズムもサポートしていますpop。関連する投稿は次のとおりです。
于 2013-08-17T16:58:25.337 に答える