我不确定我的问题是否正确。
当我使用 Z3 时，我使用 C-API 生成 Z3 约束。由于这个功能，通过编写 C 程序自动生成约束变得非常容易。因此，当我想查看约束时，我使用 C-APIZ3_solver_get_assertions以smt2格式生成约束。
现在，由于自动生成，约束线对我来说变化很大。当我想调试这些约束时，我总是必须找到特定约束的确切位置。这是一个有点乏味的任务。但是，我的问题是，我可以在 Z3 求解器中插入一个注释字符串，在我的断言之间，以便在我想转储约束时打印该字符串吗？
所以我想要的是这样的 -
Z3_Comment("Constraints of Type 1");
Z3_solver_assert(..)
..
..
Z3_solver_assert(..)
Z3_solver_assert(..)
Z3_solver_assert(..)
...
Z3_Comment("Constraints of Type 2");
Z3_solver_assert(..)
...
...
Z3_solver_assert(..)
Z3_solver_assert(..)
...
Z3_Comment("Constraints of Type 3");
Z3_solver_assert(..)
当我转储约束时，它应该打印 -
;; Constraints of Type 1
assert((..))
..
..
(assert(..))
(assert(..))
(assert(..))
...
;; Constraints of Type 2
(assert(..))
...
...
(assert(..))
(assert(..))
...
;; Constraints of Type 3
(assert(..))
也许我的问题太不现实了。
谢谢 ！