z3 - z3 中的符号变量

Question

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

1+x=c

解是 x=c-1，但 z3 总是发出一个特定的模型，比如[c = 0, x = -1]. 如何将 c“定义”为符号变量？

Answer 1

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