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）的策略。它使用高斯消元的泛化来消除变量。但是，这是一个预处理步骤，您无法控制哪些变量被消除。