Astra 版本 1.0: 评估从 Alloy 到 SMT-LIB 的翻译
软件工程
2019-06-17 v1
摘要
我们提出了多种翻译选项, 通过 Alloy 的 Kodkod 接口将 Alloy 转换为 SMT-LIB。我们的翻译实现于一个我们称之为 Astra 的库中, 其基础是将 Alloy 的集合与关系运算转换为类型化一阶逻辑 (TFOL) 中的等价形式。我们研究并比较了 SMT 求解器在多种翻译选项下的性能。我们比较了仅使用单一全类型与从 Kodkod 表示中恢复 Alloy 类型信息并在 TFOL 中使用多种类型的方法。我们比较了将关系直接翻译为 TFOL 中谓词的方法与从 Kodkod 中的关系形式恢复函数并将其表示为 TFOL 中函数的方法。我们比较了具有无界作用域的 TFOL 表示与具有有界作用域的表示 (在量词扩展之前或之后)。我们在所有这些维度上的结果为组合求解器、建模改进和优化 SMT 求解器提供了方向。
引用
@article{arxiv.1906.05881,
title = {Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB},
author = {Ali Abbassi and Nancy A. Day and Derek Rayside},
journal= {arXiv preprint arXiv:1906.05881},
year = {2019}
}