使用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. 一种确定两个布尔方程逻辑等价性的有效方法
4. 一种将布尔方程作为格式化字符串返回的方法(即，不以用于声明函数的嵌套函数形式返回。(

如果有人对其中任何一项有任何见解，我们将非常感谢您的意见。此外，如果需要进一步澄清需要什么，请告诉我。

谢谢，

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()
   

   金块som=True告诉解算器使用最小项总和。同样，根据公式的确切结构，你的里程数可能会有所不同，z3可能会引入可能无法达到目的的新名称。

3. 当然！这就是z3擅长的。只需断言f != g，其中f和g是您的方程。如果z3说unsat，那么你知道它们对于变量的所有赋值都是等价的。如果它给你一个模型，那就形成了他们平静的反例。(否定等式技巧在SMT求解中非常常见：一个公式是一个重言式，正是当它的否定不可满足时。因此，你可以断言你想要的否定，看看它是否返回unsat。(

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

4. 对于你构建的任何公式f，你都可以发布print f，它会打印出来。但正如你可能已经观察到的，它看起来不像教科书中的逻辑公式。漂亮的打印机有一些控制其行为的选项，但它可能不是你想要的。

   但是，API提供了一些函数，可以根据需要遍历AST并提取节点。所以，如果你愿意，你可以自己写一台漂亮的打印机。做到这一点并不困难，但这并不意味着它很简单：有很多情况需要考虑，根据我的经验，这样的打印机通常并不难愚弄；即对于输入的微小改变产生更糟糕的东西。

从实用的角度来看，虽然z3及其在Python、C、Java等中的高级API能够做任何你想做的事情，但除了#3之外，它不会开箱即用。我的建议是自己编写其他所有代码，并依靠z3在它擅长的地方检查相等性。当然，这完全取决于你想做什么。祝你好运！