如何更改 get-model 或 get-value 输出以打印小数而不是分数

【问题标题】：how can I change get-model or get-value output to print decimals instead of fractions如何更改 get-model 或 get-value 输出以打印小数而不是分数
【发布时间】：2014-07-10 15:29:54
【问题描述】：

当使用 SMTLIB2 文件求解时，如果我调用 get-model 或 get-value，所有内容都会打印为分数。有没有简单的方法让 Z3 打印十进制值？

例如，(get-value t) 可能会输出 ((t (/ 1.0 2.0)))，而我更喜欢 ((t 0.5)) 这样的输出。

【问题讨论】：

标签： z3

【解决方案1】：

请使用命令

(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))

【讨论】：

谢谢！是否有这些选项的列表我将来应该参考的地方？