右一套战术在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使用解决这些不等式

回答

相关问题