Z3如何将expr转换为SMT？有没有测试的方法？

Question

我经历了相关的问题，但它们没有回答我的问题。

使用Z3，cpp，我有一个表达式

expr e1=((x[0]=tru && y[0]!=tru)||(x[0]!=tru &&y[0]=tru));

tru是重言式。

[打印此表达式时，我得到

(let ((a!1 (and (or x0 (not x0)) (distinct y0 (or x0 (not x0))))))
  (or a!1 (or x0 (not x0))))

这不是我想要我的e1代表的内容。我可以以某种方式自己将expr转换为SMT，以便检查其翻译是否正确吗？还是有一种方法可以用我表示的简单方式来打印表达式，而不是使用SMT语言以有效的结构（使用子树，例如a!1等）来打印表达式？也许我可以关闭的开关？

Answer 1

某些“翻译”是不可避免的。当Z3为表达式构造解析树时，它将把它们重写为内部形式。这不仅是为了提高效率。在某些情况下，某些曲面形式也没有内部表示，而是被重写了。

当然，漂亮的印刷是另一回事。有许多方法可以控制打印效果。如果运行z3 -p并查看漂亮打印部分的输出，则会看到：

[module] pp, description: pretty printer
    bounded (bool) (default: false)
    bv_literals (bool) (default: true)
    bv_neg (bool) (default: false)
    decimal (bool) (default: false)
    decimal_precision (unsigned int) (default: 10)
    fixed_indent (bool) (default: false)
    flat_assoc (bool) (default: true)
    fp_real_literals (bool) (default: false)
    max_depth (unsigned int) (default: 5)
    max_indent (unsigned int) (default: 4294967295)
    max_num_lines (unsigned int) (default: 4294967295)
    max_ribbon (unsigned int) (default: 80)
    max_width (unsigned int) (default: 80)
    min_alias_size (unsigned int) (default: 10)
    pretty_proof (bool) (default: false)
    simplify_implies (bool) (default: true)
    single_line (bool) (default: false)

您可以使用这些设置来控制完成漂亮打印的方式，这可能更适合您的需求。特别是，从您的问题描述中，我建议设置以下两个参数：

    pp.max_depth      --> 4294967295
    pp.min_alias_size --> 4294967295

（数字实际上并不重要，只要使其足够大即可。）这两个设置应该避免漂亮打印机创建a!1子树。

不幸的是，这些选项的确切含义并没有得到充分的记录。您可以从他们的名字中猜出其中一些，而其他人则可以玩耍并观察其影响。但是，如果您真的想知道它们如何更改输出，则必须深入研究z3源代码本身。祝你好运！