使用 Z3，是否有可能以某种方式合并/简化
t>=2 or t>=1
进入
t>=1
其中 t 是一个整数？
我们希望保持对 t 的约束尽可能简单。
问问题
591 次
1 回答
3
Z3可以通过使用战术来做到这一点ctx-solver-simplify。请注意，这种策略可能非常昂贵。这种策略ctx-simplify更便宜，因为它只“传播”平等。
这是使用此策略的脚本链接： http ://rise4fun.com/Z3/F7Q
于 2012-07-16T16:32:11.060 回答