5

I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory.

Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to work well any time your decision procedures are recursive. They used to allow for plugins but that has been depricated, I think.

I'm wondering, does anybody have a recommendation of a decent SMT solver that allows you to write decision procedures for custom theories?

4

1 回答 1

8

鉴于大多数合理的 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。对于某些理论，这相当容易。参见例如 UTVPIhttps://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）来最小化您考虑的分配数量。

于 2017-10-01T20:31:14.430 回答