右一套戰術在Z3使用解決這些不等式

在此，x和k是整數和式爲：（50 < = X + KʌX + K < 51）右一套戰術在Z3使用解決這些不等式

能得到它簡化爲「x + k = 50」

我想要一套正確的策略來解決這種不平等的聯繫。

2017-02-28 Stonecipher

Z3不是簡化這種表達式的通用符號引擎。即使你有一個很好的策略組合來給你今天需要的東西，結果可能會在工具的進一步發佈中發生變化。你應該看看其他系統。即使像wolfram-alpha這樣的象徵引擎也不會產生你真正想要的;但它可能會給你一些可能更容易處理的替代形式。看到這裏：http://www.wolframalpha.com/input/?i=50%3C%3Dx%2Bk+%26%26+x%2Bk%3C51

來源

2017-03-04 23:23:22

右一套戰術在Z3使用解決這些不等式

回答

相關問題