python - 使用 Python z3 API 简化方程

Question

我正在尝试学习如何在使用 Python z3 API 中的表达式时完成一些事情。

1. 我希望能够简化/减少包含中间变量的方程组。假设我有方程 (A = B && C) 和 (C = D || E)。在 z3 中，这些将表示为 (Bool('A') == And(Bool('B'), Bool('C')) 和 (Bool('C') == Or(Bool('D'), Bool('E'))。是否有一些函数或一系列函数可用于生成简化和简化的方程 (A = B && (D || E))？
2. 我希望能够将 z3 表达式转换为乘积之和形式(即 Or(minterm1, minterm2,...)。
3. 确定两个 bool 方程逻辑等价的有效方法。
4. 一种以格式化字符串形式返回 bool 方程的方法(即不以用于声明函数的嵌套函数形式)。

如果有人对这些项目有任何见解，我们将非常感谢您的意见。另外，如果需要进一步说明所需内容，请告诉我。

谢谢

Answer 1

很好的问题。

1. 不，一般来说不是。您可以使用 z3 来简化方程，但您的“简单”概念不太可能与其内部目的所认为的简单相匹配。人们经常要求这个功能，但总的来说这是一个非常困难的问题，而且根本不清楚什么是简单。话虽如此，z3 确实有 Goal 和 Tactic 的概念，甚至还有一个 simplify 策略可供您使用。它会简化公式，但让它完全按照您希望的方式运行是一件愚蠢的事情。

   查看这个关于战术的精彩资源，也许您可​​以尝试一下以获得适合您的东西:http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

2. 我相信，简化策略确实有一个 som 选项。这可能会起作用。再次，请参阅上面的链接，其中有示例:

   s = Then(With('simplify', arith_lhs=True, som=True),
        'normalize-bounds', 'lia2pb', 'pb2bv', 
        'bit-blast', 'sat').solver()
   

   金 block som=True 告诉求解器使用 minterms 之和。同样，您的里程可能会有所不同，具体取决于公式的具体结构，并且 z3 可能会引入可能达不到目的的新名称。

3. 绝对!这就是z3所擅长的。只需断言 f != g ，其中 f 和 g 是您的方程。如果 z3 表示 unsat，那么您就知道它们对于所有变量赋值都是等效的。如果它给你一个模型，那就形成了它们等价性的反例。 (否定等式技巧在 SMT 求解中非常常见:当公式的否定不可满足时，它就是同义反复。因此，您可以断言所需内容的否定，并查看它是否返回 unsat.)

   请注意，这正是 SMT(和 SAT)求解器所擅长的。

4. 对于您构建的任何公式 f，您可以发出 print f 它会打印它。但正如您可能已经观察到的那样，它看起来不像教科书上的逻辑公式。 pretty-print 有一些选项来控制其行为，但它可能不完全是您想要的。

   但是，API 提供了按照您的意愿遍历 AST 并提取节点的函数。因此，如果您愿意，您可以编写自己的 pretty-print 。这样做并不是非常困难，但这并不意味着它很简单:有很多情况需要考虑，根据我的经验，这样的打印机通常并不难欺骗；即，对于输入的微小变化，会产生更糟糕的结果。

从实际角度来看，虽然 z3 及其 Python、C、Java 等高级 API 能够完成您想要的所有操作，但除了#3 之外，它不会是开箱即用的。我的建议是自己编写其他所有内容，并依靠 z3 来检查其擅长的相等性。当然，这完全取决于您想要做什么。祝你好运!