噸> = 1或T> = 2 => T> = 1

使用Z3，是否有可能以某種方式合併/簡化噸> = 1或T> = 2 => T> = 1

t>=2 or t>=1

成

t>=1

其中t是整數？

我們希望保持t的約束儘可能簡單。

2012-07-16 william007

Z3可以通過使用策略ctx-solver-simplify。請注意，這種策略可能相當昂貴。戰術ctx-simplify由於它只是「傳播」平等而更便宜。

下面是一個使用這種戰術腳本的鏈接： http://rise4fun.com/Z3/F7Q

2012-07-16 16:32:11

謝謝！對我來說（t> = 0和t <=1) or (t> = 0和t <=1) =>（t> = 0和t <= 1）但是爲什麼它返回鏈接的錯誤：http://rise4fun.com/Z3/aZFY – william007 2012-07-16 17:22:00

對不起，這是錯誤，我們將在下一個版本中修復它。 – 2012-07-16 18:03:57

謝謝，還有，在我看來（t> = 2和t <=2) => t == 2，但鏈接在這裏http://rise4fun.com/Z3/NHlx似乎並沒有簡化，這種簡化有可能嗎？ – william007 2012-07-16 22:49:32

回答