【发布时间】：2017-10-01 03:18:21
【问题描述】：
我正在考虑做一些验证工作，其中我将常规树语法作为基础理论。
Z3 允许您使用未解释的函数定义自己的东西，但是当您的决策过程是递归的时，这往往不会很好地工作。他们曾经允许使用插件，但我认为这已经被贬低了。
我想知道，有没有人推荐一个体面的 SMT 求解器，可以让你为自定义理论编写决策程序？
【问题讨论】：
标签： z3 verification smt formal-verification sat
【发布时间】：2017-10-01 03:18:21
【问题描述】：
鉴于大多数合理的 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。我会说使用求解器周围的外循环更容易实现第一个原型。你从求解器那里得到一个命题模型，然后检查它是否满足你的背景理论。您也可以尝试内部 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) 来尽量减少您考虑的分配数量。
【讨论】：