2

是否可以在 Z3 中禁用布尔表达式的自动简化？

例如，表达式 2 > 1 自动变为 True，而我希望它保持 2 > 1：

>>> t = 2 > 1
>>> t
True

我通过在 Z3Py 中调用 help_simplify() 找到了几个选项。但是，它们似乎都与我的问题无关。

在另一个教程（http://citeseerx.ist.psu.edu/viewdoc/download?rep=rep1&type=pdf&doi=10.1.1.225.8231）中提到了一个选项“CONTEXT SIMPLIFIER”：“此设置可用于简化子-公式判断真假。” 但是，我在 Z3Py 中找不到这个选项。

背景：我希望能够使用像 And(2>1, 1!=2) 这样的表达式，其中 2>1 和 1!=2 是较早自动生成的，有时不包含变量（常量）。Z3Py 将其简化为不被接受的 And(True, False)，因为“至少有一个参数必须是 Z3 表达式或探针”。因此，我想抑制简化。或者有没有办法让 And(True, False) 成为可接受的表达式？

提前致谢！

4

1 回答 1

1

事实上，这是因为像 2>1 这样的简单表达式被 Python 简化为 True/False。大多数运算符（如 Implies、Xor、...）对此都很好，但 And 和 Or 运算符则不然。它们有不同的实现，因为它们可以用于探针和表达式。我现在添加了更多代码，使它们的行为与其他布尔运算符一样（修复请参见此处）。我希望这可以解决这个问题，同时不会给探针带来任何新问题。如果其他人可以对此进行更多测试，我将不胜感激。

于 2014-05-29T16:36:03.470 回答