Z3Py:从方程组生成抽象公式

Question

我的例子:方程组

伪码约束基

  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约束方程组中检索此信息？

谢谢. - 如果有什么不清楚的地方,请评论一下是什么问题.

Answer 1

Z3不是提取此类信息的理想工具.在内部,它具有模块(例如,高斯消除,Groebner Basis),可用于为特定情况实现此类功能,但它们不在Z3 API中公开. Z3源代码可在线获取.

你描述的问题很有趣,但它也是非常重要的.通常,输入不仅仅是一组方程.而且,即使我们只有方程,但它们是非线性的,那么可能无法获得像你问题中描述的那样的"解决"形式.在非线性情况下,我们可以将方程式设为三角形,但就是这样.另一个问题是,即使解决方案的数量是有限的,它也不像线性情况那样独特.而且,通常,非线性方程组的解不能使用自由基来表示.在内部,Z3使用真正的代数数字来表示解.