Theta as a Horn Solver

TL;DR

This paper provides a detailed analysis of Theta, a Horn clause solver, including its algorithms, features, and performance, especially after correcting previous configuration issues, to better understand its strengths and limitations.

Contribution

It offers a comprehensive description of Theta's algorithms and features, and evaluates its performance on CHC benchmarks with corrected configurations.

Findings

Theta's core transformation approach remains effective.

Performance improved after correcting configuration issues.

Strengths and weaknesses identified in CHC-COMP benchmarks.

Abstract

Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) into control-flow automata (CFAs) for analysis -- has remained mostly unchanged, Theta's verification techniques, design trade-offs, and limitations have remained mostly unexplored in the context of CHCs. This paper fills that gap: we provide a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers. We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks. Notably, in the 2025 edition of the competition, Theta's performance was impacted by a configuration issue, leading to suboptimal results. To provide a clearer picture of Theta's actual capabilities, we re-execute the tool on the competition benchmarks under corrected settings and report on the resulting performance.