z3 中使用哪些技术来处理非线性整数实数问题？

以下是 a 的 z3 统计数据problem http://www.ccs.neu.edu/home/jaideep/example.smt2在非线性整数实数片段中（我的许多问题与此类似）：

 (:add-rows            11062574
  :added-eqs           34
  :arith-conflicts     37293
  :assert-lower        837747
  :assert-upper        1909779
  :binary-propagations 13807730
  :bound-prop          32666
  :conflicts           47631
  :decisions           157457
  :del-clause          32828
  :final-checks        39307
  :gcd-tests           329820
  :gomory-cuts         927
  :ineq-splits         19490
  :memory              39.52
  :minimized-lits      93912
  :mk-clause           73468
  :pivots              768193
  :propagations        15992318
  :pseudo-nonlinear    254856
  :restarts            41
  :time                151.65
  :total-time          151.68)

由于问题是非线性的，我相信单纯形技术不会直接用于解决这个问题（尽管我在输出中看到一些类似单纯形的统计数据）。基于一个earlier https://stackoverflow.com/questions/13102789/printing-internal-solver-formulas-in-z3响应，我了解整数存在下的非线性实数技术是基于 Grobner 基，并且相关函数位于theory_arith*。是否有一篇论文/一些文档可以让我找到有关 z3 中为此片段实现的技术的具体信息？

此外，虽然问题本身是非线性的，但唯一出现的非线性涉及两个变量的乘法（并且有一些这样的表达式），并且其中一个变量只能取 2 的幂的值，并且由一些简单的约束约束/定义：

(const1 <=  |a| < const2) => (var-a = const1)

其中 const1 和 const2 是 2 的连续正幂。因此，var-a表示小于或等于 |a| 的两个的最大幂。这些变量被声明为类型Real。 看到一个词特别好奇pseudo-nonlinear在统计输出中。约束是否以某种方式在内部线性化？另外，是否有更好的方法来编码这些约束，以便 z3 在此类问题上做得更好？

请参阅以下相关问题：

• Z3如何处理非线性整数运算？ https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic

以下内容也可能相关：

• 需要帮助理解方程 https://stackoverflow.com/questions/12326306/need-help-understanding-the-equation/12327648#12327648

• 将非线性实数与线性整数相结合 https://stackoverflow.com/questions/19661446/combining-nonlinear-real-with-linear-int

• Z3 支持非线性算术 https://stackoverflow.com/questions/18064822/z3-supports-for-nonlinear-arithmetics

• z3 处理非线性实数运算的局限性 https://stackoverflow.com/questions/13711351/z3-limitations-in-handling-nonlinear-real-arithmetics