2

yices で行うのと同様に、z3 でコンテキストをリセットしたい: void yices_reset (yices_context ctx) z3 に相当するコマンドはありますか? 現在私は使用していますZ3_del_context(ctx);が、それが最も効率的な方法であるかどうかはわかりません。push/pop コンテキスト コマンドを使用する必要がありますか、それとも別の方法がありますか?

4

1 に答える 1

4

Z3_del_context(ctx)はオプションです。ただし、質問では、プッシュ/ポップについて言及しています。したがって、実際にはアサーションのセットだけをリセットしたいようです。その場合は、Z3_solverオブジェクトの使用を開始することをお勧めします。オブジェクト内にさまざまなZ3_solverオブジェクトを作成できZ3_contextます。主な利点は、宣言、式、式などを共有できることです。ところで、Z3 には C++ ラッパー ( z3++.h) が付属しており、C API をより簡単に使用できます。複数のソルバー オブジェクトを使用する C++ の例を次に示します。ところで、同時に複数のソルバー オブジェクトを使用できます。

context c;
expr x = c.int_const("x");
expr y = c.int_const("y");
{
   solver s(c);

   s.add(x >= 1);
   s.add(y < x + 3);
   std::cout << s.check() << "\n";

   model m = s.get_model();
   std::cout << m << "\n";
   // solver object c will be destroyed at this point
}
{
   // creating a new solver object
   solver s2(c);
   s2.add(x > y + 1);
   std::cout << s2.check() << "\n";
}

EDIT : ソルバー オブジェクトにもresetメソッドがあります。特定のソルバーでアサートされたすべてのアサーションを消去します。

于 2012-11-01T15:16:05.270 に答える