Reasoning about Data Trees using CHCs

Reasoning about data structures requires powerful logics supporting the combination of structural and data properties. We define a new logic called Mso-D (Monadic Second-Order logic with Data) as an extension of standard Mso on trees with predicates of the desired data logic. We also define a new class of symbolic data tree automata (SDTA) to deal with data trees using a simple machine. Mso-D and SDTA are both Turing-powerful, and their high expressiveness is necessary to deal with interesting data structures. We cope with undecidability by encoding SDTA executions as a system of CHCs (Constrained Horn Clauses) and solving the resulting system using off-the-shelf solvers. We also identify a fragment of Mso-D whose satisfiability can be effectively reduced to the emptiness problem for SDATAs. This fragment is very expressive since it allows us to characterize a variety of data trees from the literature, solving certain infinite-state games, etc. We implement this reduction in a prototype tool that combines an Mso decision procedure over trees (Mona) with a CHC engine (Z3), and use this tool to conduct several experiments, demonstrating the effectiveness of our approach across different problem domains.