# Finding Regular Herbrand Models for CHCs using Answer Set Programming

Grégoire Maire, Thomas Genet

► To cite this version:

Grégoire Maire, Thomas Genet. Finding Regular Herbrand Models for CHCs using Answer Set Programming. HCVS 2025 - 12th Workshop on Horn Clauses for Verification and Synthesis, Emanuele De Angelis, Florian Frohn, Jul 2025, Zagreb, Croatia. hal-05459509

HAL Id: hal-05459509

https://inria.hal.science/hal-05459509v1

Submitted on 15 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Finding Regular Herbrand Models for CHCs using Answer Set Programming

Grégoire Maire

ENS Rennes

gregoire.maire@ens-rennes.fr

Thomas Genet

Univ Rennes, IRISA, Inria

genet@irisa.fr

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. Kostyukov & al. [5] have shown how to derive an automaton when CVC4 finds a finite model. 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.

We are interested in the automatic verification of programs manipulating Algebraic Data Types (ADTs). The analysis of such programs is challenging as soon as the ADTs are recursive because they define unbounded data structures. When ADTs are recursive, tree automata [1] provide an efficient way to finitely represent unbounded sets of such ADTs. In [6, 3, 4, 5], verifying a property $\phi$ on a program $P$ consists in building a tree automaton recognizing a set of all the computations of the program and in checking that the property is true on this set. When $P$ is represented by a set of functions (resp. a term rewriting system), the property $\phi$ is expressed as a set of results that should not be reachable when applying the semantics of $P$ on initial function calls (resp. rewriting initial terms with $P$). In this setting the tree automaton finitely represents the set of all values (resp. terms) that are reachable when applying the semantics of $P$ (resp. rewriting with $P$). In the context of program verification using Constrained Horn Clauses (CHC for short), this is adapted as follows: $P$ is represented by a set of Horn clauses and the property $\phi$ is a negative formula, i.e., $\phi \stackrel{def}{=} (\psi \Rightarrow \perp)$. To prove that $P \Rightarrow (\psi \Rightarrow \perp)$ is valid, we build a tree automaton finitely representing the least Herbrand model $M$ of $P$ and we check that the formula $\psi$ does not hold in $M$. This entails that $\psi$ is not a logical consequence of $P$. Thus, $P \Rightarrow (\psi \Rightarrow \perp)$ is valid.

For instance, let $nat = z | s(nat)$ be the ADT defining natural numbers. Let $P$ be the set of CHCs defining $even(x)$ and $odd(x)$ as the usual predicates over numbers and $plus(x,y,z)$ as the predicate such that $z = x+y$. Let $\phi_1 \stackrel{def}{=} \forall x y z. even(x) \land even(y) \land plus(x,y,z) \land odd(z) \Rightarrow \perp$ be the (negative) property we want to prove on $P$. Since the ADT of natural numbers is recursive, Herbrand models of $P$ are unbounded. However, we can finitely represent such an unbounded model using a tree automaton:

$$ 
\begin{array}{lclcl}
z & \to & \#2 & odd(\#1) & \to & \#0 & plus(\#1, \#2, \#1) & \to & \#0 \\
s(\#2) & \to & \#1 & even(\#2) & \to & \#0 & plus(\#1, \#1, \#2) & \to & \#0 \\
s(\#1) & \to & \#2 & plus(\#2, \#1, \#1) & \to & \#0 & plus(\#2, \#2, \#2) & \to & \#0
\end{array}
$$

In this automaton, #0, #1, #2 are the states of the automaton. A term is recognized by a state if it can be rewritten to this state using the transitions. For instance, the state #2 recognizes the term $z$, the state #1 recognizes $s(z) \to s(\#2) \to \#1$, i.e., #2 recognizes even numbers and #1 recognizes odd numbers. Finally, the state #0 recognizes all the atoms that are true in the considered Herbrand model, e.g, $even(s(s(z)))$, $odd(s(z))$. Note that the model recognized by this automaton is not the least Herbrand model but an over-approximation. In particular, this automaton recognizes $plus(s(z), s(z), s(s(z)))$ which is part of the
least Herbrand model but also plus(s(z), s(z), z) which is not. On this model, the property $\phi_1$ is true. In particular, with the rule plus(#2,#2,#2) → #0 we can see that summing two even numbers always result into an even number. Since the negative property $\phi_1$ is true on an over-approximation of the least Herbrand model then it is also true on the least Herbrand model.

To infer such an automaton, Kostyukov & al. [5] use the finite model finder of CVC4. They transform the input problem ($P \wedge \phi$) over the theory of ADTs into a problem in the Equality Logic with Uninterpreted Functions (EUF). Then, if there exists a finite model of the problem in EUF, they show how to derive a tree automaton recognizing an Herbrand model in the ADT theory satisfying $P \wedge \phi$ and proving $P \Rightarrow \phi$.

In this paper, we report preliminary experiments on an alternative way to build such an automaton by an encoding into a SAT problem using Clingo [2], an Answer Set Programming (ASP) tool. Given a set of Prolog-style clauses, Clingo searches for a Herbrand model of this set of clauses. Unlike usual Prolog interpreter, Clingo is guaranteed to terminate and outputs the Herbrand models as soon as the models are finite. However, how discussed above, the Herbrand models we look for are *not* finite but can be *finitely* represented using tree automata. Here is a possible encoding of $P$ and $\phi_1$ in Clingo. We first set the maximal number of states in the automaton we search for.

```c
#const maxState=2.
state(1..maxState). % this shortcut builds facts state(1). and state(2).
```

The following lines define the tree automaton rules for the abstraction of the ADT. We encode a rule of the form $s(#1) \rightarrow #2$ by the fact `rule(s(1), 2)`. The automaton we want to build for terms of the ADT is expected to be complete (any term should be recognized by *at least* one state) and deterministic (any term should be recognized by *at most* one state). This is easily encoded using Clingo's cardinality constraints.

```c
1 {rule(z, Q): state(Q)} 1.
1 {rule(s(Q0), Q): state(Q)} 1 :- state(Q0).
```

In the first line above, the brackets around the fact `rule(z,Q)` mean that this fact may or may not appear in the searched model. By adding 1 on the left, we impose that *at least* one fact of this kind appears in the model. By adding 1 on the right we impose that *at most* one fact of this form appears in the model. The annotation `state(Q)` forces Q to be one of the states. Thus, if a model is found it will necessarily have exactly one fact `rule(z,1)` or `rule(z,2)` (since we have here only 2 states). The second line ensures there is exactly one state Q such that $s(Q_0) \rightarrow Q$ for all states $Q_0$. The following lines essentially give the types and cardinality of the relations *even*, *odd* and *plus*. We provide those information but we want to infer the relation themselves. Again, because of the brackets, these lines only say that those facts may or may not appear in the model.

```c
{even(Q0)} :- state(Q0).
{odd(Q0)} :- state(Q0).
{plus(Q0, Q1, Q2)} :- state(Q0), state(Q1), state(Q2).
```

Finally, we can state the CHCs of our satisfiability problem. They are directly translated into Clingo's clauses where terms are replaced by the corresponding states and transitions. For instance, one clause defining the *even* predicate is `even(s(X)) :- odd(X)`. In the encoding, since predicates ranges over states and not terms, we cannot directly represent an atom over the term `s(X)`. Instead, we encode this using several facts, i.e., a state $Q_1$ and a rule $s(Q_0) \rightarrow Q_1$. This results into the following set of Clingo clauses.

```c
even(Q0) :- rule(z, Q0).      % even(z).
even(Q2) :- odd(Q1), rule(s(Q1), Q2). % even(s(X)) :- odd(X).
```
```
odd(Q2) :- even(Q1), rule(s(Q1), Q2).              % odd(s(X)) :- even(X).
plus(Q1, Q0, Q0) :- rule(z, Q1), state(Q0).        % plus(z, X, X).
                 % plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
plus(Q6, Q3, Q7) :- plus(Q1, Q3, Q5), rule(s(Q1), Q6), rule(s(Q5), Q7).
                 % :- even(X), even(Y), plus(X, Y, Z), odd(Z).
:- even(Q0), even(Q1), plus(Q0, Q1, Q2), odd(Q2).
```

We prototyped this translation and the satisfiability checking in OCaml and Clingo: https://gitlab.inria.fr/regular-pv/regularmodels. The translation is very close to the one above except that it also uses a predicate `stateType(Q,t)` to distinguish states w.r.t. the type `t` of the terms they recognize. Another difference is that bodies of initial CHCs may contain equalities $X = Y$ or disequalities $X! = Y$ ranging over terms. Equalities can be encoded by equalities on states because the automaton is deterministic: if terms are equal then so are the states. However, note that different terms may be recognized by the same state. Hence, the body of the clause may be true on states though it is not on the recognized terms. This results into an over-approximation of the Herbrand model which is safe w.r.t. the property that is a negative clause. On the opposite, encoding term disequalities by state disequalities is not safe: a disequality $X! = Y$ in the body may be satisfied by two different terms $t_1$ and $t_2$ though they are recognized by the same state. This would result into an under-approximation of the Herbrand model which is not safe. As a result we define the `diffApprox(Q1, Q2)` predicate over-approximating the `! =` relation on terms. This predicate is true if $Q1$ and $Q2$ recognizes at least two different terms.

Finally, our satisfiability procedure generates Clingo specifications with increasing values of `maxStates` until one solution is found. For each value of `maxStates`, we generate two specifications: one for satisfiability checking and another (with small modifications) to search for a counterexample. Note that, given a value of `maxStates`, if Clingo fails to find a model (and if Clingo is complete) then we have a guarantee that there exists no regular Herbrand model that can be recognized by an automaton of `maxStates`.

Thus, by iteratively increasing `maxStates`, we have a semi-complete tool to check for satisfiability of CHCs with ADTs: if there exists a regular Herbrand model we will find it. This was also the case with [5] where semi-completeness relies on completeness of CVC4 finite model-finder. Since Clingo's solving core is pure SAT-solving our encoding with Clingo could be more efficient than [5]. This has to be investigated further. To improve efficiency, we also plan to have a modular solving based on the Regular Language Typing approach of [4].

**Acknowledgements** Many thanks to Théo Losekoot for fruitful discussions about Clingo.

## References

[1] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison & M. Tommasi (2008): *Tree Automata Techniques and Applications*. http://tata.gforge.inria.fr.

[2] M. Gebser, R. Kaminski, B. Kaufmann & T. Schaub (2019): *Multi-shot ASP solving with clingo*. TPLP 19(1), pp. 27–82.

[3] T. Genet, T. Haudebourg & T. Jensen (2018): *Verifying Higher-Order Functions with Tree Automata*. In: FoSSaCS’18, LNCS 10803, Springer.

[4] T. Haudebourg, T. Genet & T. Jensen (2020): *Regular Language Type Inference with Term Rewriting*. In: ICFP’20, 4, ACM, pp. 112:1–112:29. Available at https://doi.org/10.1145/3408994.

[5] Y. Kostyukov, D. Mordvinov & G. Fedyukovich (2021): *Beyond the Elementary Representations of Program Invariants over Algebraic Data Types*. In: PLDI ’21, ACM, pp. 451–465.

[6] Y. Matsumoto, N. Kobayashi & H. Unno (2015): *Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs*. In: APLAS’15, LNCS 9458, Springer, pp. 295–312.