>>> conclusion
Implies(And(Not(Exists(z, R(z, e3))),  
            Not(Exists(z, R(z, e2)))),  
        And(Not(B(e3)), Not(B(e2))))  
>>> conclusion.sexpr()  
'(let ((a!1 (and (not (exists ((z Ent)) (R z e3)))\\n                (not (exists ((z Ent)) (R z e2))))))\\n  (=\> a!1 (and (not (B e3)) (not (B e2)))))'

如你所见，字符串形式（__str__）中的变量 conclusion 以 Implies 开头，而 sexpr 形式以 let 开头。

为什么它们不同？字符串形式和S-expr形式在什么时候会不同？

我在参考文献中也找不到线索。

不仅是我，这份演示文稿 也指出了 Z3 sexpr 与 string 之间的差异，但并未解释清楚。

解决方案

当你执行

print(conclusion)

Z3正在输出表达式的内部表示。它是表达式的基于Python的数据类型表示。你看到的只是Python层对表达式的呈现。

当你执行

print(conclusion.sexpr())

z3将表达式打印为 SMT-Lib格式。SMT-Lib是所有符合规范的SMT求解器都接受的标准表示，与之相比，你看到的AST完全是z3特定的表示。

所以，它们打印出来的结果不同，原因是第一种情况下你得到的是z3的内部特定AST，便于在Python中操作z3表达式；而在后者你得到的是所有求解器都能理解的标准表示；这是一种完全不同的语言。

关于使用 let

z3尝试通过共享来最小化输出，正如你所猜测的，这些表达式很快就会变得非常大。如果你不想看到这种效果，只需执行：

set_option("pp.min_alias_size", 1000000)
set_option("pp.max_depth",      1000000)

在打印之前，输出应该大致是扁平的（除非它真的非常深。你可以调整这些数字来适应你对美化输出的偏好。）

完整运行示例

你没有给出完整的脚本，所以我重新创建了一个看起来差不多的。如下代码按原样工作：

from z3 import *

z  = Int('z')
e2 = Int('e2')
e3 = Int('e3')
B = Function('B', IntSort(), BoolSort())
R = Function('R', IntSort(), IntSort(), BoolSort())

conclusion = Implies(And(Not(Exists(z, R(z, e3))),
                         Not(Exists(z, R(z, e2)))),
                     And(Not(B(e3)), Not(B(e2))))

set_option("pp.min_alias_size", 1000000)
set_option("pp.max_depth",      1000000)

print(conclusion.sexpr())

把上面的内容放到一个名为 a.py 的文件中并运行它，我得到：

$ python a.py
(=> (and (not (exists ((z Int)) (R z e3))) (not (exists ((z Int)) (R z e2))))
    (and (not (B e3)) (not (B e2))))