t＞＝1或t＞＝2＝＞t＞＝1 [英] t>=1 or t>=2 => t>=1

问题描述

使用Z3，是否有可能以某种方式合并/简化

Using Z3, is it possible to somehow merge/simplify

t>=2 or t>=1

进入

t>=1

其中 t 是整数?

我们希望对 t 的约束尽可能简单.

We wish keep the constraint for t as simple as possible.

推荐答案

Z3 可以通过使用策略 ctx-solver-simplify 来做到这一点.请注意，这种策略可能非常昂贵.策略 ctx-simplify 更便宜，因为它只传播"平等.

Z3 can do it by using the tactic ctx-solver-simplify. Note that this tactic may be quite expensive. The tactic ctx-simplify is cheaper by it only "propagates" equalities.

这是使用此策略的脚本链接:http://rise4fun.com/Z3/F7Q

Here is a link for script using this tactic: http://rise4fun.com/Z3/F7Q

这篇关于t＞＝1或t＞＝2＝＞t＞＝1的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！