z3 - 转换为“set-option”SMTLib 格式

Question

我想将此 z3py 代码（在线代码）转换为标准 SMTLib 格式。除了设置选项属性 " (set-option :produce-models true) (set-option :timeout 4000)"之外，所有内容都转换为 SMTLib 格式。为什么不工作？转换代码由 Leonardo de Moura 提出。

我希望输出像 -

; benchmark 
(set-info :status unknown)
(set-option :produce-models true)
(set-option :timeout 4000)
(set-logic QF_UFLIA)
(assert true)
(check-sat)

谢谢

Answer 1

SMT-LIB2 漂亮打印机不打印选项。漂亮的打印机返回一个字符串，您应该能够预先选择您选择的选项。

Answer 2

我正在运行你的代码，我正在获取

; benchmark
(set-info :status unknown)
(set-logic QF_UFLIA)
(assert true)
(check-sat)