English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present a variety of translation options for converting Alloy to SMT-LIBvia Alloy's Kodkod interface. Our translations, which are implemented in alibrary that we call Astra, are based on converting the set and relationaloperations of Alloy into their equivalent in typed first-order logic (TFOL). Weinvestigate and compare the performance of an SMT solver for many translationoptions. We compare using only one universal type to recovering Alloy typeinformation from the Kodkod representation and using multiple types in TFOL. Wecompare a direct translation of the relations to predicates in TFOL to onewhere we recover functions from their relational form in Kodkod and representthese as functions in TFOL. We compare representations in TFOL with unboundedscopes to ones with bounded scopes, either pre or post quantifier expansion.Our results across all these dimensions provide directions for portfoliosolvers, modelling improvements, and optimizing SMT solvers.

Astra Version 1.0: Evaluating Translations from Alloy to SMT-LIB