新博客文章：我写的一些傻乎乎的Z3脚本

# 新博客文章：我写的一些蠢萌 Z3 脚本 来源：https://buttondown.com/hillelwayne/archive/new-blog-post-some-silly-z3-scripts-i-wrote 既然现在我不再把所有时间花在《Logic for Programmers》上，就有时间更新我的网站了！所以，这是五个月来的第一篇博客文章：[一些我写的蠢萌 Z3 脚本](https://www.hillelwayne.com/post/z3-examples/)。 通常我还会放一个 Patreon 笔记的链接，但我决定不再喜欢发布付费内容，并且打算逐步关闭那整个功能。所以，关于这篇文章的一些简短说明： * 部分目的诚然是为《LfP》的最终发布造势。我想开始宣传这本书，但又不希望宣传材料毫无趣味，所以一些与之相关但独立的博客文章是一个很好的起点。 * 这篇文章讨论了“冗余内容”（chaff）这个概念，即大量未能收录进书中的素材（包括代码示例和散文）。这本书大约有 5 万字……而且比总量庞大的“冗余内容”短得多！我 *不认为* 大部分内容可以转化为有用的公开文章，但我也不完全反对这个想法。也许有些老章节可以改造成点什么？ * 构思一个需要证明的条件数学性质相当困难。我有两个候选：`a == b * c => a / b == c`，这需要大篇幅讨论为什么 Z3 中的除法必须是总量的；以及 `a != 0 => some b: b * a == 1`，这需要引入一个量词（SMT 在处理量词方面真的很奇怪）。除以零的问题已经给我带来了足够多的麻烦，所以我选择了后者。这意味着在讨论数组时，我必须重新引入“操作必须是总量的”这一概念。 * 我完全不知道为什么数组示例返回的利润最大值是 `2` 而不是 `99999999`。我猜是当问题定义不明确时，优化器存在某种短路逻辑？ * 有一个例子我没能让它工作，这很可惜：将哥德巴赫猜想编码为 SMT 问题，以此展示 SMT 求解器是不可判定的。任何包含多层嵌套量词的问题都很棘手。 *如果你是在网页上读到这篇文章，可以[在此订阅](https://buttondown.com/hillelwayne)。每周更新一次。我的主站是[这里](https://www.hillelwayne.com/)。* *我的新书《Logic for Programmers》现已进入早期访问阶段！[在此获取](https://leanpub.com/logic/)。*