z3 - LRA 下量词消除的最新求解器是什么？

Question

我已经在线性实数算术下尝试了 Z3 的量词消除。该公式不是很大，但是当要消除的变量数超过 5 时，它需要很长时间（或永远不会终止）。是否存在其他可以做得更好的求解器？或者有什么技巧可以帮助Z3？

Answer 1

我不是专家，但您可以尝试使用 RedLog 的 Reduce。