Z3 中的优化：删除 epsilon

Question

优化受严格约束（例如max x s.t. x < 4）的实际值会在对Z3_optimize_get_upper 的调用中生成epsilon 值。

在上面的例子中，返回值是4 - epsilon。

有没有办法摆脱 epsilon，即将它实例化为任何特定值？例如。将其设置为0、1 或0.1？

谢谢！

编辑：

在opt_context.cpp的代码中，我看到创建了名为epsilon的常量：

if (!eps.is_zero()) { expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_int());

Answer 1

实际上，我已经想通了：使用substitute 并进一步调用simplify 似乎可以解决问题。