Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB
Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB
复制标题
Astra 版本 1.0：评估从合金到 SMT-LIB 的翻译
DOI：
10.1007/978-3-662-46675-9_20
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Derek Rayside
中科院分区：
文献类型：
--
作者：
Ali Abbassi;N. Day;Derek Rayside
我们提供了多种转换选项，用于通过合金的Kodkod接口将合金转换为SMT-Lib。我们的翻译是在一个我们称为Astra的库中实现的，它基于将Crystal的集合和关系操作转换为类型化一阶逻辑(TFOL)中的等价操作。我们研究并比较了SMT求解器在多种翻译选项下的性能。我们将仅使用一个通用类型与从Kodkod表示中恢复合金类型信息与使用TFOL中的多个类型进行比较。我们将TFOL中的关系到谓词的直接转换与从Kodkod中的关系形式恢复函数并将其表示为TFOL中的函数的转换进行比较。我们将具有无界作用域的TFOL中的表示与具有有界作用域的表示进行比较，无论是在量词扩展之前还是之后。我们在所有这些方面的结果都为投资组合解算器、模型改进和优化SMT解算器提供了方向。
We present a variety of translation options for converting Alloy to SMT-LIB via Alloy's Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational operations of Alloy into their equivalent in typed first-order logic (TFOL). We investigate and compare the performance of an SMT solver for many translation options. We compare using only one universal type to recovering Alloy type information from the Kodkod representation and using multiple types in TFOL. We compare a direct translation of the relations to predicates in TFOL to one where we recover functions from their relational form in Kodkod and represent these as functions in TFOL. We compare representations in TFOL with unbounded scopes to ones with bounded scopes, either pre or post quantifier expansion. Our results across all these dimensions provide directions for portfolio solvers, modelling improvements, and optimizing SMT solvers.