是否有增量 SMT 求解器或某些增量 SMT 求解器的 API，我可以在其中增量添加约束，在其中我可以通过某些标签/名称唯一标识每个约束？
我想唯一地标识约束的原因是，我可以稍后通过指定该标签/名称来删除它们。需要删除约束是因为我之前的约束随着时间变得无关紧要。我看到使用 Z3 我不能使用基于推送/弹出的增量方法，因为它遵循基于堆栈的想法，而我的要求是删除特定的早期/旧约束。使用基于假设的 Z3 的其他增量方法，我将不得不执行格式“(check-sat p1 p2 p3)”的 check-sat，即如果我有三个断言要检查，那么我将需要三个布尔常量 p1,p2 ,p3，但在我的实现中，我一次要检查数千个断言，间接需要数千个布尔常量。我还检查了 JavaSMT，一个用于 SMT 求解器的 Java API，
我想知道是否有任何增量求解器可以添加或删除由名称唯一标识的约束，或者有其他方法来处理它的 API。我将不胜感激任何建议或意见。