  We study Satisfiability Modulo Theories (SMT) enriched with the so-called
Ramsey quantifiers, which assert the existence of cliques (complete graphs) in
the graph induced by some formulas. The extended framework is known to have
applications in proving program termination (in particular, whether a
transitive binary predicate is well-founded), and monadic decomposability of
SMT formulas. Our main result is a new algorithm for eliminating Ramsey
quantifiers from three common SMT theories: Linear Integer Arithmetic (LIA),
Linear Real Arithmetic (LRA), and Linear Integer Real Arithmetic (LIRA). In
particular, if we work only with existentially quantified formulas, then our
algorithm runs in polynomial time and produces a formula of linear size. One
immediate consequence is that checking well-foundedness of a given formula in
the aforementioned theory defining a transitive predicate can be
straightforwardly handled by highly optimized SMT-solvers. We show also how
this provides a uniform semi-algorithm for verifying termination and liveness
with completeness guarantee (in fact, with an optimal computational complexity)
for several well-known classes of infinite-state systems, which include
succinct timed systems, one-counter systems, and monotonic counter systems.
Another immediate consequence is a solution to an open problem on checking
monadic decomposability of a given relation in quantifier-free fragments of LRA
and LIRA, which is an important problem in automated reasoning and constraint
databases. Our result immediately implies decidability of this problem with an
optimal complexity (coNP-complete) and enables exploitation of SMT-solvers. It
also provides a termination guarantee for the generic monadic decomposition
algorithm of Veanes et al. for LIA, LRA, and LIRA. We report encouraging
experimental results on a prototype implementation of our algorithms on
micro-benchmarks.
