Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
A preliminary version of this work was published in the proceedings of IJCAR 2020 . The current article extends the original versions with complete proofs, as well as a discussion and results regarding existential theories (see Proposition 2). Additionally, Sect. 5 is extended to provide a more comprehensive treatment of axiomatizations for trees.