Z3Py：从方程系统生成抽象公式答案

【问题标题】：Z3Py: Generating Abstract Formulas From A System Of EquationsZ3Py：从方程系统生成抽象公式
【发布时间】：2013-02-28 20:38:35
【问题描述】：

我的例子：方程组

伪代码约束库

  a = b+c
∧ e = a*c

∧ a = +2     ; some replaceable concrete values
∧ c = +18

解决方案

  b = -16
∧ e = -32

我想要的信息

在方程组中，我想得到以下知识：

抽象公式，我可以使用它根据给定值（在约束基础中）计算变量值（解决方案）。

（就像在高中时，老师不仅希望看到结果，还希望看到这样一个转换的抽象公式。）

公式...

  b = a-c     ; is an equivalent transformation from `a = b+c`
∧ e = (a-c)*c ; is an term replacement `b → a-c` of `e = a*c`

我的问题

如何使用 Z3Py 从 Z3 约束方程系统中检索此信息？

谢谢。 - 如果有任何不清楚的地方，请就问题所在发表评论。

【问题讨论】：

标签： math constraints z3 proof theorem-proving

【解决方案1】：

Z3 并不是提取此类信息的理想工具。在内部，它有一些模块（例如，高斯消除，Groebner Basis）可能对在特定情况下实现这种功能很有用，但它们没有在 Z3 API 中公开。 The Z3 source code is available online.

你描述的问题很有趣，但也不是微不足道的。一般来说，输入不仅仅是一组方程。此外，即使我们只有方程，但它们是非线性的，那么也可能无法获得像您的问题中描述的那样的“已解决”形式。在非线性情况下，我们可以将方程组以三角形形式表示，但仅此而已。另一个问题是，即使解决方案的数量是有限的，它也不像线性情况那样是唯一的。此外，一般来说，非线性方程组的解不能用根式表示。在内部，Z3 使用real algebraic numbers 表示解决方案。

【讨论】：