使用 SMTLIB2 文件求解时,如果我调用 get-model 或 get-value,一切都将打印为分数。有没有一种简单的方法可以让 Z3 打印十进制值?
例如, (get-value t)
可能会输出 ((t (/ 1.0 2.0)))
,而我更喜欢 ((t 0.5))
之类的东西。
最佳答案
请使用命令
(set-option :pp.decimal true)
请看下面的例子
(declare-const t Real)
(assert (= t (/ 1.0 2.0)))
(check-sat)
(set-option :pp.decimal true)
(get-model)
(get-value (t))
和相应的输出是
sat (model (define-fun t () Real 0.5) )
((t 0.5))
关于z3 - 如何更改 get-model 或 get-value 输出以打印小数而不是分数,我们在Stack Overflow上找到一个类似的问题:https://stackoverflow.com/questions/24680561/