z3 - 具有自定义理论的 SMT 求解器？

Question

我正在考虑做一些验证工作，其中我有常规的树语法作为基础理论。

Z3 允许您使用未解释的函数定义自己的东西，但是当您的决策过程是递归的时，这往往不会很好地工作。他们曾经允许使用插件，但我认为这已经被贬低了。

我想知道，有没有人推荐一个体面的 SMT 求解器，可以让你为自定义理论编写决策程序？

Answer 1

鉴于大多数合理的 SMT 求解器都是开源的，因此有多种选择，您可以根据需要花费多少时间和精力，在任何细节上集成理论求解器。

OpenSMT http://verify.inf.usi.ch/opensmt专为实现可插拔理论集成而构建。

VeriT、Yices 和 CVC4 是开源的，您可以查看这些求解器中的理论集成。

Z3 是开源的，可让您和其他人在其上进行构建。有一个用于 DPLL(T) 插件模式的 API，但是当 Z3 的源代码开放时我们删除了它，而且还有一个基本限制:它不能很好地支持模型构建。用于插入理论的内部 API 原则上与外部 API 同构。一篇较早的论文描述了各种整合理论的方法是 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-aplas11.pdf .我会说使用求解器周围的外循环更容易实现第一个原型(prototype)。你从求解器那里得到一个命题模型，然后检查它是否满足你的背景理论。您也可以尝试内部 API。对于某些理论，这相当容易。参见例如 UTVPI https://github.com/Z3Prover/z3/blob/master/src/smt/theory_utvpi_def.h作为样本。对于弦理论，它相当复杂(因为该理论需要大量的特殊情况推理)。模块 z3str3 在今年早些时候被集成 https://github.com/Z3Prover/z3/blob/master/src/smt/theory_str.cpp , 开发仍在进行中。大约是10KLOC。 Bui Phi Dep 使用旧版本的 Z3 进行外部理论集成 https://github.com/diepbp/FAT .这也是大量的代码，再次因为字符串和转换器理论需要相当多的设置。对于愿意响应用户错误报告和请求的贡献者，我们 (Z3) 非常欢迎对 Z3 的主要分支做出额外贡献，其中包含未涵盖的理论和算法。在字符串和树接受器/转换器空间中有相当多的摆动空间。

同样，我想说，对于第一个版本，您应该在外部集成方面取得相当大的进展，让 SMT 求解器处理命题 SAT 和未解释的函数(如果需要，还可以进行算术运算)。然后，您可以向求解器询问模型并添加理论公理，直到您从求解器返回的命题模型与您的理论一致(或者您得到 UNSAT)。
并非命题模型中的所有分配都是相关的。您可以通过应用双重传播 ( http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/29_niemetz.pdf) 来最小化您考虑的分配数量。