使用 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/

10-11 23:19
查看更多