z3(python)表达式操作入门

1、首先，如图这段代码定义了一个名为expr的表达式，并且使用print_expr函数来显示表达式的详细信息。

3、如图编写了一个visit_expr函数，用于递归地访问表达式，并显示各个子表达式的信息。

5、编写如图一个简单的函数，用于手动将一个表达式变换为原来的非（将And变为Or，并将各个子式变为原来的非）。

7、我们可以用ctx-solver-simplify用求解器进行化简，可以看到表达式取反的结果是正确的。