我正在研究一个项目,其重点是使用术语重写来解决/简化固定大小的位向量算术问题,这对于某些决策程序(例如基于钻头爆破的程序)的先前步骤是有用的.术语重写可以完全解决问题,或者产生更简单的等效问题,因此两者的组合可以导致相当大的加速.
我知道许多SMT求解器实现了这种策略(例如Boolector,Beaver,Alt-Ergo或Z3),但很难找到详细描述这些重写步骤的论文/技术报告/等.一般来说,我只发现了作者在几段中描述这种简化步骤的论文.我想找一些文件详细解释术语重写的用法:提供规则的例子,讨论AC重写和/或其他等式公理的便利性,重写策略的使用等.
目前,我刚刚找到了技术报告"固定宽度位向量的决策程序",描述了CVC Lite执行的规范化/简化步骤,我想找到更多这样的技术报告!我还发现了一张关于STP术语重写的海报,但这只是一个简短的总结.
我已经访问了那些SMT求解器的网站,我在他们的出版物页面中搜索过......
我将不胜感激任何参考,或任何有关如何在当前版本的知名SMT求解器中使用术语重写的解释.我对Z3特别感兴趣,因为它看起来有一个最聪明的简化阶段.例如,Z3 3.*引入了一个新的位向量决策程序,但遗憾的是,我无法找到任何描述它的论文.