0

この z3py コード (オンライン コード) を標準の SMTLib 形式に変換したいと考えています。set options プロパティ " (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)

ありがとう

4

2 に答える 2

1

オプションは、SMT-LIB2 プリティ プリンタでは印刷されません。きれいなプリンターは文字列を返し、選択したオプションを前に保留できるはずです。

于 2013-09-11T01:50:50.733 に答える