Abstract: Constraint answer set programming integrates ASP with constraint processing  enabling powerful declarative encodings of complex combinatorial search problems. System EZSMT is an extensible constraint answer set programming framework that advances the translational approach to CASP solving. It utilizes satisfiability modulo theory solvers for search, while providing the benefits of a high-level declarative programming paradigm. In other words, it can be seen as a tool that simplifies the use of SMT solvers by enabling it with logic programming interface. In addition, EZSMT extends the language of logic programs under answer set semantics with new modeling capabilities.  Indeed, the unique feature of this system is  its ability to process linear constraints simultaneously containing integer and real variables.  The system provides a robust platform for future extensions and theoretical exploration within the CASP domain.  In particular, it builds upon the developments in the CLINGO 5 series that promotes the extensibility philosophy. The CLINGO 5 system provides means to elaborate the specifications for new kinds of constructs to be incorporated for processing within its grounding tool GRINGO. EZSMT takes advantage of this feature. In the talk we will discuss theoretical and practical underpinnings of the framework as well as present some benchmark information positioning the system among its peers.

Abstract: Highly optimized ASP solvers deliver outstanding performance, but their tightly engineered internals make them ill-suited for quickly prototyping new language featmetaspr exploring alternative semantics. Meta-programming offers a way out of this rigidity: by reifying a program's syntax as facts and reinterpreting them through declarative encodings, researchers can experiment with novel language constructs natively within ASP, without touching solver internals. This tutorial introduces participants to meta-programming as a general methodology for customizing and extending the ASP workflow, showing how reification and meta-encodings turn solver customization into an accessible, declarative exercise rather than a systems-engineering one.

Building on these foundations, the second part of the tutorial turns to the temporal domain. We present metasp, a flexible meta-programming framework that operationalizes the semantics of varied temporal logics through a unified, declarative framework. Our approach extends standard ASP meta-programming by augmenting clingo's theory grammar with formal type specifications and nesting capabilities. To ensure semantic correctness, we introduce a transformation pipeline that protects nested modalities from stable-model-based simplifications during grounding. Through hands-on examples, participants will see how metasp lets them define and adapt temporal logics declaratively, sidestepping the architectural rigidity of monolithic systems.

A key enabler behind metasp's flexibility is aspen, a system for reifying, transforming, and analyzing non-ground ASP source code — addressing a gap left by traditional meta-programming approaches, which operate only on ground programs. Built on tree-sitter, aspen parses source code into a reified fact base, applies clingo-driven meta-encodings to generate transformation instructions, and rewrites source via a templating engine — enabling the very preprocessing pipeline that lets metasp extend clingo with new temporal constructs. We will walk through concrete aspen case studies, to illustrate how non-ground transformation and analysis work in practice.

This tutorial aims to lower the barrier to entry for extending ASP: by the end, participants should feel equipped to prototype their own language extensions using metasp and aspen as accessible, hands-on tools for exploration rather than black boxes.