在 z3py 中设置单项式次数

Question

在推理多项式不等式时，Z3 似乎必须首先将多项式转换为单项形式。我想知道求解器中是否有一个设置可以让我定义我希望多项式转换为的单项次数？

我用的是z3py界面，网上搜索找不到。

Answer 1

不，Z3 没有这个设置。