I am not sure, if my question is correct.
When I use Z3, I generate the Z3 constraints using C-API. Due this this facility, it is become extremely easy to generate the constraints automatically by writing a C-program. So when I want to see the constraints I use the C-API Z3_solver_get_assertions to generate the constraints in the smt2 format.
Now, due to automatic generation the lines of constraints vary for me quite a lot. When I want to debug these constraints, I always have to find where exactly a specific constraint is. This is a little tedious task. However, my question is that, can I insert a comment string in the Z3 solver, in between my assertions such that it will print that string when I want to dump the constraints?
so what I would like is something like this -
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(..)
and when I dump the constraints it should print -
;; Constraints of Type 1
assert((..))
..
..
(assert(..))
(assert(..))
(assert(..))
...
;; Constraints of Type 2
(assert(..))
...
...
(assert(..))
(assert(..))
...
;; Constraints of Type 3
(assert(..))
Maybe my question is too un-realistic.
Thanks !