CODEWITHSUNDEEP
z3
Raj
Raj

Reputation: 3462

Inserting a comment string in Z3

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 !

Upvotes: 1

Views: 902

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The Z3 API does not provide this functionality. I think the easiest solution is to create your own data-structure for storing expressions+comments. You can do it by using a list/array of expression/string.

Upvotes: 1

Related Questions