z3 - Z3中多线性有理算术的量词消除

Question

据我了解，Z3 在遇到量化线性实数/有理算术时，应用了 Bjørner、IJCAR 2010 以及 Bjørner 和 Monniaux 最近的工作中描述的量词消除形式（qe_sat_tactic.cpp至少是这么说的）。

我想知道

1. 如果公式是多线性的，它是否仍然有效，因为“常数”是象征性的。例如∀x, ax≤b ⇒ ax≤0可以通过分离a<0、a=0和a>0的情况来处理。这可以使用 Weispfenning 的虚拟替换方法，但我不知道最终在 Z3 中实现了什么（也就是说，它是实现通用方法还是仅限于常数系数的方法）。

2. 是否有可能在 Z3 中输出消除结果，而不仅仅是求解一个模型。这样做可能有 Z3 策略，但我不知道应该如何请求。

3. 是否有可能在 Z3 中进行上述消除，然后使用新的非线性求解器来获得模型。同样，一连串的策略可能会奏效，但我不知道应该如何请求。

谢谢。

Answer 1

经过长途旅行（包括我在一次会议上遇到大卫的旅行），这里有一个简短的摘要来回答提出的问题。

1. 没有对多线性形式的特定支持。
2. 'qe' 策略会产生消除的结果，但可能会作为副作用决定可满足性。
3. 这是一个非常有趣的调查问题，但不支持开箱即用。