z3 - z3 上下文重置 API

Question

我想在 z3 中重置上下文，类似于我在 yices 中所做的：Z3void yices_reset (yices_context ctx) 是否有等效命令？目前我使用Z3_del_context(ctx);但我不确定这是最有效的方法。我应该使用推送/弹出上下文命令，还是有其他方法？

Answer 1

Z3_del_context(ctx)是一种选择。但是，在您的问题中，您提到了 push/pop。因此，您似乎实际上只想重置一组断言。如果是这样的话，我建议你开始使用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";
}

编辑：求解器对象也有一个reset方法。它擦除在给定求解器中断言的所有断言。