Astra: Evaluating Translations from Alloy to SMT-LIB

Abstract

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 have three translation axes, and in total, twelve different combinations. 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.

We propose characteristics for classifying problems, which we hypothesize affect the performance. We provide a set of test cases with different characteristics, and by testing our translation on our tests, we create a statistical model to correlate characteristics to the performance of different translation options. We propose hypotheses regarding SMT solvers and modelling guidelines, and test them based on our empirical results. Our results across all these dimensions provide directions for portfolio solvers, modelling improvements, and optimizing SMT solvers.

At the end, we present a set of questions that suggest future work. These questions are based on results we could not justify or find a reason for. The subjects of these questions are SMT solvers and modelling optimizations.