z3 中的符号变量

【问题标题】：Symbolic variables in z3z3 中的符号变量
【发布时间】：2012-06-27 10:16:30
【问题描述】：

有没有办法让 z3 求解器发出“符号”解？例如，对于方程：

1+x=c

解决方案是 x=c-1，但 z3 总是发出特定的模型，例如 [c = 0, x = -1]。如何将c“定义”为符号变量？

【问题讨论】：

【解决方案1】：

不幸的是，Z3 没有公开这种功能。尽管我们在内部使用求解器，但它们并未在 API 中公开。在未来的版本中，我们希望公开内部组件，例如：求解器、Grobner 基础程序等。在当前版本中，我们有一个称为solve-eqs 的策略（参见http://rise4fun.com/Z3Py/tutorial/strategies）。它使用高斯消除的推广来消除变量。但是，这是一个预处理步骤，您无法控制消除哪些变量。

【讨论】：

对此有何更新？ Z3 4.5版本中是否有获取符号解的API？