本文介绍了t＞＝1或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的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！