在Z3中插入註釋字符串

Question

我不確定，如果我的問題是正確的。

當我使用Z3時，我使用C-API生成Z3約束。由於這個功能，通過編寫C程序自動生成約束變得非常容易。所以當我想看到約束時，我使用C-API Z3_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(..)) 

也許我的問題是過於非現實的。

謝謝！

Answer 1

Z3 API不提供而不是提供此功能。我認爲最簡單的解決方案是創建自己的數據結構來存儲表達式+註釋。你可以通過使用表達式/字符串的列表/數組來完成。