【发布时间】：2013-07-13 18:10:52
【问题描述】：
据我了解，Z3 在遇到量化线性实数/有理算术时，会应用 Bjørner、IJCAR 2010 以及 Bjørner 和 Monniaux 最近的工作中描述的量词消除形式（至少 qe_sat_tactic.cpp 是这么说的） )。
我想知道
如果公式是多线性的，它是否仍然有效，因为“常数”是象征性的。例如。 ∀x, ax≤b ⇒ ax≤0 可以通过分离 a0 的情况来处理。使用 Weispfenning 的虚拟替换方法可以做到这一点，但我不知道最终在 Z3 中实现了什么（也就是说，它是实现通用方法还是仅限于常数系数的方法）。
是否可以在 Z3 中输出消除结果，而不仅仅是求解一个模型。这样做可能有 Z3 策略，但我不知道应该如何请求。
是否可以在 Z3 中执行上述消除，然后使用新的非线性求解器获得模型。同样，一连串的策略可能会奏效，但我不知道应该如何请求。
谢谢。
【问题讨论】：
-
如果我理解你的正确，并且正确地阅读了你的名字（+链接），你实际上是在问一些关于你描述自己的方法的非常具体的问题。抱歉，我们无法告诉您您的工作可以做什么，不能做什么。此外，问题似乎不是特定的编程问题。 （如果我误解了你，这是一个提示你重新制定它）。
-
大卫，弗洛洛可能有一点。我们可以/应该通过电子邮件讨论这个问题，或者使用 Z3 网站上的讨论环节：z3.codeplex.com/discussions
-
fiolo，我只是不知道最终在 Z3 中实现了什么；描述一个算法和知道它是如何在一个不是你设计的系统中结束的有很大的区别。 ;-) 我也不知道传递给 Z3 以要求线性量词消除然后是一般非线性求解的正确请求顺序。也不知道有没有什么方法可以要求z3输出量词剔除的结果……