使用Python z3 API简化方程式 [英] Simplifying Equations with Python z3 API

问题描述

我正在尝试学习在Python z3 API中使用表达式时如何完成一些工作.

I'm trying to learn how to accomplish a few things when working with expressions in the 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. 一种将布尔方程返回为格式化字符串的方式(即不是以用于声明函数的嵌套函数形式).

1. I would like to be able to simplify/reduce sets of equations that contain intermediate variables. Say I have the Equations (A = B && C) and (C = D || E). In z3 these would be represented as (Bool('A') == And(Bool('B'), Bool('C')) and (Bool('C') == Or(Bool('D'), Bool('E')). Is there some function or series of functions that can be used to produce the simplified and reduced equation (A = B && (D || E))?
2. I would like to be able to convert a z3 expression into sum of products form (i.e Or(minterm1, minterm2,...).
3. An efficient way of determining the logical equivalence of two boolean equations.
4. A way of returning a boolean equations as formatted strings (i.e NOT in the nested function form used to declare the function.)

如果任何人对这些项目有任何了解，将非常感谢您的投入.另外，如果需要进一步澄清所需内容，请告诉我.

If anyone has any insight on any of these items, your input would be very much appreciated. Also, if any further clarification as to what is desired is needed, please let me know.

谢谢

推荐答案

好问题.

1. 不，一般来说不是.您可以使用z3来简化方程式，但是简单"的概念不太可能与出于内部目的而认为简单的匹配.人们通常会要求使用此功能，但这通常是一个非常棘手的问题，并且根本不清楚简单"的含义.话虽如此，z3确实具有 Goal 和 Tactic 的概念，甚至还可以使用 simplify 策略.它将简化公式，但是让它精确地执行您希望其执行的方式是傻瓜的事.

1. No, not in general. You can get z3 to simplify equations, but your notion of "simple" is unlikely to match what it will consider simple for its internal purposes. People often ask for this feature, but it is in general a very hard problem, and not at all clear what's meant by simple. Having said that, z3 does have a notion of Goal and Tactic, and there is even a simplify tactic that you can use. It will simplify the formulas, but having it behave precisely the way you want it to behave is a fool's errand.

查看有关此战术的大量资源，也许您可​​以四处看看，以获取对您有用的东西:

See this great resource on tactics and perhaps you can play around to see to get something that works for you: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm

简化策略确实有 som 选项.这可能会奏效.同样，请参见上面的链接，其中包含示例:

The simplify tactic does have a som option, I believe. That might do the trick. Again, see the above link, where they have the example:

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

掘金 som = True 告诉求解器使用最小和.同样，您的里程数可能会根据公式的确切结构而有所不同，z3可能会引入可能会破坏目的的新名称.

The nugget som=True tells the solver to use sum-of-minterms. Again, your mileage might vary depending on the exact structure of your formulas, and z3 might introduce new names that might defeat the purpose.

绝对！这就是z3擅长的.只需声明 f！= g ，其中 f 和 g 是您的方程式.如果z3表示 unsat ，那么您知道它们对于变量的所有分配都是等效的.如果它为您提供了一个模型，那将成为其等同性的反例.(求等式的技巧在SMT解决中很常见:公式恰好在其否定式不满足时才是重言式.因此，您可以断言想要的取反，并查看它是否返回 unsat .)

Absolutely! This is what z3 excels at. Simply assert f != g where f and g are your equations. If z3 says unsat, then you know they are equivalent for all assignments to variables. If it gives you a model, that forms a counter-example to their equaivalence. (The negated-equality trick is very common in SMT solving: A formula is a tautology precisely when its negation is unsatisfiable. So, you can assert the negation of what you want and see if it comes back with unsat.)

请注意，这就是SMT(和SAT)求解器的优势所在.

Note that this is what SMT (and SAT) solvers excel at.

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

For any formula f you build, you can issue print f and it'll print it. But as you probably already observed, it will not look like your textbook logical formulas. The pretty-printer has some options to control its behaviour, but it's probably not quite what you want.

但是，API提供了一些功能，可以按照需要移动AST并提取节点.因此，您可以根据需要编写自己的漂亮打印机.这样做并不是很困难，但这并不意味着它很简单:有很多情况需要考虑，根据我的经验，这样的打印机通常并不难被愚弄.也就是说，如果对输入进行细微的更改，则会产生更糟糕的结果.

However, the API provides functions to walk down the AST and extract nodes as you wish. So, you can write your own pretty printer if you so desire. Doing so isn't terribly difficult, but that doesn't mean it's simple: There are many cases to consider and in my experience, such printers are usually not that hard to fool; i.e., produce something vastly worse for small changes to the input.

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

From a practical perspective, while z3 and its high-level APIs in Python, C, Java, etc., is capable of doing everything you want, it's not going to be out-of-the-box except for #3. My recommendation would be to code everything else yourself, and rely on z3 for checking equality where it excels at. Of course, this all depends on precisely what you're trying to do. Best of luck!

这篇关于使用Python z3 API简化方程式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！