具有自定义理论的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.我想说使用求解器周围的外环可以更容易地实现第一个原型.你从求解器得到一个命题模型,然后检查它是否满足你的背景理论.您也可以尝试内部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).