z3 - t>=1またはt>=2 => t> = 1

Question

Z3を使用して、どういうわけかマージ/簡素化することは可能ですか？

t>=2 or t>=1

の中へ

t>=1

ここで、tは整数ですか？

tの制約をできるだけ単純に保つことを望みます。

Answer 1

Z3は戦術を使用してそれを行うことができますctx-solver-simplify。この戦術はかなり費用がかかる可能性があることに注意してください。戦術ctx-simplifyは、平等を「伝播」するだけで安価です。

この戦術を使用したスクリプトへのリンクは次のとおりです。http： //rise4fun.com/Z3/F7Q