SMT解决方案与自定义理论？
问题描述：
我在做一些验证工作，我已经将常规树语法作为基础理论。SMT解决方案与自定义理论？
Z3允许您定义自己的东西与未解释的函数，但是，如果您的决策过程是递归的，那么这种方法并不适用。他们曾经允许使用插件，但我认为这已经被删除了。
我想知道，有没有人有一个体面的SMT解决方案的建议，让你写定制理论的决策程序？
答
考虑到最合理的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）最大限度地减少分配的数量。