2025/10/30 by Maire, Gregoire, Genet, Thomas
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2510.26428
We are interested in proving satisfiability of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). We propose to prove satisfiability by building a tree automaton recognizing the Herbrand model of the CHCs. If such an automaton exists then the model is said to be regular, i.e., the Herbrand model is a regular set of atoms. Kostyukov et al. have shown how to derive an automaton when CVC4 finds a finite model of the CHCs. We propose an alternative way to build the automaton using an encoding into a SAT problem using Clingo, an Answer Set Programming (ASP) tool. We implemented a translation of CHCs with ADTs into an ASP problem. Combined with Clingo, we obtain a semi-complete satisfiability checker: it finds a tree automaton if a regular Herbrand model exists or finds a counter-example if the problem is unsatisfiable.