如何避免将大型 z3 表达式转换为 python 中的省略号？

Question

我有一个字符串格式的大 z3 BitVec 表达式。要将其转换为 BitVec 格式的表达式，我使用了 'eval()'。但是，表达式变成了省略号。我该如何避免这种情况？

from z3 import *


a0=BitVec('a0',1)
a1=BitVec('a1',1)
c0=BitVec('c0',1)
c1=BitVec('c1',1)

b=BitVec('b',1)


d=BitVec('d',1)
f=BitVec('f',1)
g=BitVec('g',1)
e=BitVec('e',1)
h=BitVec('h',1)
a=BitVec('a',1)
c=BitVec('c',1)


exp = '(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)|f|(a&b&c)|(c&d&e&f&g)|(a1&a0&c1&c0)|(g&h)'

print(eval(exp))

输出 ::
... |... |... |... |... |... |... |... |... |... |... |... |.. . |... |... |... |... |... |... |... |... |... |... |... |... | ... |... |... |... |... |... |... |... |... |... |... |... |.. . |... |... |... |... |... |... |... |... |... |... |... |... | ... |... |... |... |... |... |... |... |... |... |... |... |.. . |... |... |... |... |... |... |... |... |... |... |... |... | ... |... |... |... |... |... |... |... |... |... |... |... |.. . |... |... |... |... |... |... |... |... |... |... |... |... | ... |... |... |... |... |... |... |...

Answer 1

椭圆由 z3 中的漂亮打印机设置控制。您可以在程序顶部的import 语句之后添加以下行：

set_option(max_args=100000000, max_lines=10000000, max_depth=100000000, max_visited=10000000)

这通常适用于足够小的问题。问题是漂亮的打印机使用了相当低效的算法来执行此操作，如果您在示例中尝试上述方法，您会发现 z3 几乎要花很长时间才能打印您的表达式；所以它并不能真正解决你的问题。

另一种选择是打印与您的表达式相对应的 s 表达式，而不是以更类似于 python 的格式打印它。为此，请将最后一行更改为：

print(eval(exp).sexpr())

在这种情况下，您会发现 z3 会快速打印输出，尽管输出可能不如您预期的那么“漂亮”。 （特别是，它使用全括号前缀表示法；而不是更熟悉的减少括号的中缀表示法。）然而，在我看来，它非常易读，并且可能在这里做正确的事情。