具有自定义理论的SMT求解器? [英] SMT solver with custom theories?

问题描述

我正在做一些验证工作，在这些工作中我将常规树语法作为基础理论.

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

Z3允许您使用未解释的函数来定义自己的东西，但是在您的决策过程是递归的时候，这往往无法正常工作.我认为他们曾经允许使用插件，但是已经过时了.

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.

我想知道，有没有人建议过像样的SMT求解器，使您可以编写自定义理论的决策程序?

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

推荐答案

鉴于最合理的SMT求解器是开源的，因此您有多种选择，您可以根据需要花费的时间和精力来详细集成理论求解器.

There are several options given that most reasonable SMT solvers are open source you can integrate theory solvers in any detail depending on how much time and energy you have to spend.

• OpenSMT http://verify.inf.usi.ch/opensmt 专门用于实现可插拔理论集成.
• VeriT，Yices和CVC4是开源的，您可以在这些求解器中进行理论整合.
• Z3是开源的，可用于使您和其他人在此基础上构建.有一个用于DPLL(T)插件模式的API，但是我们在Z3的源代码公开时将其删除，并且由于一个基本限制:它不支持模型构建.用于插入理论的内部API原则上与外部API同构.较旧的文章描述了各种整合理论的方法， 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的主要分支做出额外的贡献.字符串和树接受器/换能器空间中有很大的摆动空间.

• OpenSMT http://verify.inf.usi.ch/opensmt was specifically built to enable pluggable theory integration.
• VeriT, Yices and CVC4 are open source and you could look into theory integration in these solvers.
• Z3 is open source and is available to enable you and others to build on it. There was an API for a DPLL(T) plugin mode, but we removed it when Z3's source became open and also due to a basic limitation: it didn't support model construction well. The internal APIs used for plugging in theories are in principle isomorphic to the external APIs. An older paper describing various ways to integrate theories is https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-aplas11.pdf. I would say a first prototype is much easier achieved using an outer loop around the solver. You get a propositional model from the solver and then check if it satisfies your background theory. You can also try the internal APIs. For some theories, this is fairly easy. See for example UTVPI https://github.com/Z3Prover/z3/blob/master/src/smt/theory_utvpi_def.h as a sample. For the theory of strings, it is fairly involved (because the theory requires substantial special case reasoning). The module z3str3 was integrated earlier this year https://github.com/Z3Prover/z3/blob/master/src/smt/theory_str.cpp, and development is still ongoing. It is about 10KLOC. Bui Phi Dep uses the older version of Z3 for an external theory integration https://github.com/diepbp/FAT. It is also a substantial amount of code, again as strings and transducer theories require quite a bit of setup. For contributors who are willing to be responsive to user bug reports and requests we (Z3) very much welcome additional contributions to the main branch of Z3 with theories and algorithms that are not covered. There is quite a bit of wiggle room in the string and tree acceptor/transducer space.

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

Again, I would say that for a first version you should get pretty far with an external integration where you let the SMT solver deal with propositional SAT and uninterpreted functions (and arithmetic if you need this). You can then ask the solver for a model and add theory axioms back until the propositional model you get back from the solver aligns with your theory (or you get UNSAT). Not all assignments in the propositional model are going to be relevant. You can minimize the number of assignments you consider by applying dual propagation (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/29_niemetz.pdf).

这篇关于具有自定义理论的SMT求解器?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！