基于“堆栈”的方法在 SMTLib 中已经根深蒂固，因此我认为很难找到一个完全满足您需求的求解器。尽管我确实同意这将是一个很好的功能。
话虽如此，我可以想到两个解决方案。但两者都不能很好地满足您的特定用例，尽管它们都会work。归根结底，您希望能够在每次调用时挑选约束条件check-sat。不幸的是，这会很昂贵。每次求解器执行check-sat it learns许多基于所有当前断言的引理，以及许多内部数据结构都进行了相应的修改。基于堆栈的方法本质上允许求解器“回溯”到这些学习状态之一。但是，当然，这不允许像您观察到的那样进行挑选。
所以，我认为你只剩下以下之一：
使用 check-sat-假设
这基本上就是您已经描述的内容。但回顾一下，您只需给它们命名，而不是断言布尔值。所以这：
(assert complicated_expression)
becomes
; for each constraint ci, do this:
(declare-const ci Bool)
(assert (= ci complicated_expression))
; then, check with whatever subset you want
(check-sat-assuming (ci cj ck..))
这确实增加了您必须管理的布尔常量的数量，但从某种意义上说，这些都是您想要的“名称”。我知道您不喜欢这样，因为它引入了很多变量；事实确实如此。这是有充分理由的。请参阅此处的讨论：https://github.com/Z3Prover/z3/issues/1048 https://github.com/Z3Prover/z3/issues/1048
使用重置断言和：全局声明
这是一个变体，允许您在每次调用时任意挑选断言check-sat。但它会not便宜点。特别是，每次您按照此方法进行操作时，求解器都会忘记所学到的所有内容。但它会完全按照您的意愿行事。首要问题：
(set-option :global-declarations true)
并以某种方式在你的包装中自己跟踪所有这些。现在，如果您想任意“添加”约束，则无需执行任何操作。只需添加它即可。如果你想删除某些东西，那么你可以说：
(reset-assertions)
(assert your-tracked-assertion-1)
(assert your-tracked-assertion-2)
;(assert your-tracked-assertion-3) <-- Note the comment, we're skipping
(assert your-tracked-assertion-4)
..etc
等等。也就是说，你“删除”你不想要的那些。请注意，:global-declarations调用很重要，因为它将确保您调用时所有数据声明和其他绑定保持完整reset-assertions，它告诉求解器从其假设和学到的内容开始。
实际上，您正在管理自己的限制，正如您最初所希望的那样。
Summary
这些解决方案都不是您想要的，但它们都会起作用。如果不诉诸这两种解决方案之一，就没有符合 SMTLib 的方法可以完成您想要的操作。然而，个别求解器可能还有其他技巧。您可能需要咨询他们的开发人员，看看他们是否有针对此用例的定制内容。虽然我怀疑情况确实如此，但很高兴能找到答案！
另请参阅 Nikolaj 之前的回答，该回答非常相关：Z3 中的增量求解如何工作？ https://stackoverflow.com/questions/16422018/how-incremental-solving-works-in-z3?rq=1
