Optimal CHC Solving via Termination Proofs
YU GU, University of Tsukuba, Japan
TAKESHI TSUKADA, Chiba University, JapanHIROSHI UNNO, University of Tsukuba, Japan and RIKEN AIP, Japan
Motivated by applications to open program reasoning such as maximal specification inference, this paper
studies optimal CHC solving, a problem to compute maximal and/or minimal solutions of constrained Hornclauses (CHCs). This problem and its subproblems have been studied in the literature, and a major approachis to iteratively improve a solution of CHCs until it becomes optimal. So a key ingredient of optimization
methods is the optimality checking of a given solution.
We propose a novel optimality checking method, as well as an optimization method using the proposed
optimality checker, based on a computational theoretical analysis of the optimality checking problem. The key
observation is that the optimality checking problem is closely related to the termination analysis of programs,
and this observation is useful both theoretically and practically. From a theoretical perspective, it clarifies
a limitation of an existing method and incorrectness of another method in the literature. From a practicalperspective, it allows us to apply techniques of termination analysis to the optimality checking of a solutionof CHCs. We present an optimality checking method based on constraint-based synthesis of terminationarguments, implemented our method, evaluated it on CHCs that encode maximal specification synthesis
problems, and obtained promising results.
CCS Concepts: • Theory of computation → Logic and verification; Automated reasoning; Program
verification.
Additional Key Words and Phrases: specification synthesis, termination analysis, constrained Horn clause
ACM Reference Format:
Yu Gu, Takeshi Tsukada, and Hiroshi Unno. 2023. Optimal CHC Solving via Termination Proofs. Proc. ACM
Program. Lang. 7, POPL, Article 21 (January 2023), 28 pages. https://doi.org/10.1145/3571214

1

INTRODUCTION

Specification synthesis is an enabling technique for modular verification of open programs whichinteract with other libraries and user programs; Open library functions can be invoked arbitrarily
by unknown user programs, and conversely open user programs invoke library functions as blackboxes. Depending on the assumptions on the type of interactions between the target programand its environment, specification synthesis takes various forms such as sufficient precondition
inference [Padhi et al. 2016; Sankaranarayanan et al. 2008; Seghir and Kroening 2013; Srivastava
and Gulwani 2009], angelic verification [Blackshear and Lahiri 2013; Das et al. 2015; Lahiri et al.
2020], and maximal specification synthesis [Albarghouthi et al. 2016; Prabhu et al. 2021; Zhou et al.
2021].
This paper focuses on a variant of maximal specification synthesis, namely computation of
maximal solutions of a given set of constrained Horn clauses (CHCs). Since our idea to compute a
Authors’ addresses: Yu Gu, University of Tsukuba, Japan, kou@logic.cs.tsukuba.ac.jp; Takeshi Tsukada, Chiba University,
Japan, tsukada@math.s.chiba-u.ac.jp; Hiroshi Unno, University of Tsukuba, Japan and RIKEN AIP, Japan, uhiro@cs.tsukuba.
ac.jp.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/1-ART21
https://doi.org/10.1145/3571214

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21

21:2

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

maximal solution is applicable to synthesizing a minimal solution, we shall study the problem tocalculate maximal and/or minimal solution of a given set of CHCs. We call this class of problems
Constrained Horn Clause optimization (or CHC optimization). This subsumes problems such as
multi-abduction [Albarghouthi et al. 2016] and maximal CHC solving [Prabhu et al. 2021].
The key ingredient of our optimal solution synthesis method is a novel optimality checker thatguarantees the optimality via constraint-based synthesis of termination arguments; Our optimality
checking method is derived based on a computational theoretical analysis of the problem of deciding
the optimality of a given solution for (subclasses of) CHC optimization problems: we show that
optimality checking can be reduced to pfwCSP [Unno et al. 2021] that extends CHCs with non-Hornclauses, well-foundedness, and functionality constraints. The analysis also reveals a limitation ofexisting methods [Albarghouthi et al. 2016; Hashimoto and Unno 2015; Srivastava and Gulwani2009], i.e. there exists a problem which cannot be solved by existing methods. It also proves theunsoundness of an optimality checking method [Prabhu et al. 2021].1
Our CHC optimization method iteratively refines the current solution of the given CHCs C
until an optimal one is found. To this end, we solve a series C0, C1, C2, . . . of constraint sets where
C0 = C and each C𝑖+1 (𝑖 ≥ 0) is obtained from C by adding a constraint that specifies that any
solution of C𝑖+1 strictly improves the solution found for C𝑖 . To express C𝑖+1 (𝑖 ≥ 0), we introduce
and use a new class of predicate constraint satisfaction problems that extends CHCs with nonemptiness constraints on predicate variables. Our theoretical analysis shows that the new class iscomputationally easier than that of existentially quantified CHCs [Beyene et al. 2013] that has beenused for the same purpose by the previous predicate constraint optimization method [Hashimotoand Unno 2015].
This paper further presents a data-driven approach to automating the constraint-based optimality
checking and specification refinement. Specifically, we present a method based on CounterExample Guided Inductive Synthesis (CEGIS) [Solar-Lezama et al. 2006] and stratified families oftemplates [Unno et al. 2021] for solving a new class pfwnCSP of predicate constraint satisfaction
problems that extends pfwCSP with non-emptiness constraints.
We implemented our specification synthesis method, evaluated it on a diversity of specification
synthesis problems, and obtained promising results: despite the computational hardness of optimality checking, our method synthesized optimal specifications for non-trivial programs. Thus
our novel approach to optimality checking via termination proofs, along with the computational
theoretical analysis, paves the way for future directions of optimal specification synthesis.
Organization of This Paper. The rest of the paper is organized as follows. Section 2 presents a brief
overview of our approach to optimal specification synthesis. Section 3 defines the class of CHC
optimization problems and its subclasses. Section 4 gives the theoretical analysis of the (subclassesof) CHC optimization. Section 5 derives our optimality checking method based on termination
proofs from the observations in the theoretical analysis. Section 6 formalizes our CHC optimization
procedure by introducing the class pfwnCSP of predicate constraint satisfaction problems, which isused in the three sub-procedures: constraint-based optimality checking, constraint-based solution
refinement (or non-optimality checking), and pfwnCSP solving. We report on our implementationand evaluation of the presented method in Section 7 and compare it with related work in Section 8.
We conclude the paper with some remarks on future work in Section 9.

1 It is worth noting and emphasizing here that the main technical contents of Prabhu et al. [2021] are heuristic methods

that aim to construct a “practically useful” solution, which are independent of the flaw in their optimality checker. It also
discusses a way to weaken a given solution.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:3

a = rand1∀ (); b = rand2∀ ();assert(not 𝑆(a,b))
def f(x):y = rand();if 𝑆(x,y) thenreturn yelse diverge

def f(x):y = rand3∃ ();if 𝑆(x,y) or (x,y)=(a,b) thenreturn yelse diverges = 0; i = 0;
while * do
if * thens = s + f(i);else
i = i + 1;
assert(s >= 0);

s = 0; i = 0;
while * do
if * thens = s + f(i);else
i = i + 1;
assert(s >= 0);

s = 0; i = 0;
while rand4∃ () doif rand5∃ () thens = s + f(i);else
i = i + 1;
assert(s >= 0);(a) Example of an input program.

(b) Reduction of the sufficiency of 𝐹 to the safety verification.

(c) Reduction of the maximality of 𝐹 to theangelic-demonic reachability analysis.

Fig. 1. Example of a maximal specification inference problem and reduction of the sufficiency and maximality
checking to program analysis.

2

OVERVIEWThis section provides the idea of the method of this paper. The main contribution of this paper is anapplication of the termination analysis of programs to the CHC optimization problem. We explain
why the termination analysis is relevant, as well as differences between our approach and existing
methods [Albarghouthi et al. 2016; Zhou et al. 2021], using examples of the maximal specification
inference problem [Albarghouthi et al. 2016], which is closely related to the CHC optimization
problem via the well-known relationship between programs and CHCs.
Maximal Specification Inference
The maximal specification inference problem asks, given a program with assertions and an externalfunction f, to give a maximal (i.e. weakest) specification for f among those ensuring the safety ofthe program. Following [Albarghouthi et al. 2016], we assume that a specification of a function
f : D → D ′ is a predicate 𝐹 over D × D ′. A function f satisfies this specification if and only if
𝐹 (𝑥, f(𝑥)) holds for every 𝑥 ∈ D. A specification 𝑆 is sufficient if the program is safe whenever the
implementation of f satisfies 𝑆. Otherwise it is insufficient. The goal of the maximal specification
inference is to find a maximal specification (with respect to the standard subset ordering) among
sufficient specifications.
An example of the input program is shown in Figure 1a. Specifications 𝑆 1 (𝑥, 𝑦) :⇔ (𝑥 ≥ 0 ⇒𝑦 ≥ 0) and 𝑆 2 (𝑥, 𝑦) :⇔ (𝑦 = 0) are sufficient, and 𝑆 3 (𝑥, 𝑦) :⇔ (𝑥 ≥ 10 ⇒ 𝑦 ≥ 0) is insufficient. A
maximal specification is 𝑆 1 , which is actually the unique maximal specification for the program in
Figure 1a. There may be more than one maximal specification in general.
We construct a maximal specification by iteratively improving sufficient specifications. Let 𝑆 0 bea sufficient specification. We check if 𝑆 0 is maximal, and if it is not, we construct another sufficient
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:4

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

specification 𝑆 1 that is strictly larger than 𝑆 0 . We iterate this process until a maximal specification
is found. The key step is the maximality check.
Sufficiency Checking as Program Analysis
The sufficiency of a given specification 𝑆 is reducible to the safety verification of a program. The
idea is to give an implementation of the “external” function f that is the “worst” among thosesatisfying 𝐹 . The “worst” implementation isdef f(x):y = rand();if 𝑆(x,y) then return y else diverge
which nondeterministically returns a value following the specification 𝑆. This is the “worst” inthe sense that, if the input program with this implementation is safe, then so is the program with
arbitrary implementation of f that satisfies 𝑆. Hence 𝑆 is sufficient if and only if the program in
Figure 1b is safe.
Note that this idea of the reduction is applicable to check whether 𝑆 is insufficient: 𝑆 is insufficient
if and only if the program in Figure 1b is unsafe. So the insufficiency of a specification can be
reduced to the reachability problem,2 which is the dual of the safety verification problem.
Maximality Checking as Program Analysis
The maximality checking is also reducible to program analysis, although the result of the reduction
is a more difficult problem. Let 𝑆 be a specification, which we would like to prove to be maximal. If
𝑆 is maximal, for every pair (𝑎, 𝑏) such that ¬𝑆 (𝑎, 𝑏), the extension 𝑆𝑎,𝑏 (𝑥, 𝑦) :⇔ (𝑆 (𝑥, 𝑦) ∨ (𝑥, 𝑦) =(𝑎, 𝑏)) is insufficient:
𝑆 is maximal⇐⇒∀(𝑎, 𝑏) ∈ D × D ′ .

¬𝑆 (𝑎, 𝑏) implies 𝑆𝑎,𝑏 is insufficient.

For a given (𝑎, 𝑏), the insufficiency checking of 𝑆𝑎,𝑏 is reducible to the reachability analysis of acertain program. Describing the universal quantifier ∀(𝑎, 𝑏) ∈ D × D ′ as a program results in asingle program of which the reachability problem is equivalent to the maximality of 𝑆.
Figure 1c is the resulting program. It first chooses the pair (𝑎, 𝑏) ∈ D × D ′, nondeterministically,such that ¬𝑆 (𝑎, 𝑏). Then it executes the input program with the “worst” implementation of f withrespect to 𝑆𝑎,𝑏 . The resulting program (Figure 1c) is nondeterministic. It is worth noting here thatthe program of Figure 1c has two kinds of nondeterministic branches:3• The nondetermenistic choices of 𝑎 and 𝑏 are demonic, that means, we should prove that the
program reaches the assertion failure whatever the choices of 𝑎 and 𝑏 are.
• All other nondeterministic choices are angelic, that means, we should find appropriate choices
so that the program reaches the assertion failure.
By this way, the maximality checking is reduced to the reachability analysis of a program withangelic and demonic nondeterministic branches.
Once the maximality problem is reduced to the reachability analysis of a program, a variety ofreachability analysis methods [Beyene et al. 2014; Cook et al. 2006; Fedyukovich et al. 2018; Giesl
et al. 2017; Gonnord et al. 2015; Heizmann et al. 2014; Kura et al. 2021; Kuwahara et al. 2014; Leeet al. 2001; Unno et al. 2021; Urban et al. 2016] become applicable to solve the problem. A standard
2 We do not distinguish the reachability problem and the termination problem, which asks reachability to the end of the

program.
3 The meaning of angelic and demonic choices might be counter-intuitive. In the terminology here, reaching an assertion
failure is regarded as a good event because the maximality of a given specification is equivalent to the assertion failure forevery proper extension of the specification.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofsa = rand1∀ (); b = rand2∀ ();assert(a >= 0 and b < 0)
def f(x):y = b;
if (x < 0 or y >= 0) or (x,y)=(a,b)
then return yelse diverge

21:5

s = 0; i = 0;
while i <= a do
if a == i and s >= 0 thens = s + f(i);else
i = i + 1;
assert(s >= 0);

Fig. 2. Program in Figure 1c with particular specification 𝑆 = 𝑆 1 and particular implementations of rand ∃ ().

technique is to reduce the reachability analysis to the safety verification problem by finding anappropriate ranking function [Alias et al. 2010; Ben-Amram and Genaim 2014, 2017; Bradley et al.
2005; Leike and Heizmann 2014; Podelski and Rybalchenko 2004; Urban 2013; Urban and Miné 2014],
which gives an upper bound of the number of steps needed to reach the desired program point.
A slight difference from a common setting is that the program in Figure 1c has not only demonic
branches but also angelic nondeterministic choices rand𝑖∃ (). We remove rand𝑖∃ () by replacing
it with an appropriate concrete function choice𝑖 (®
𝑥), which may depend on the arguments 𝑥®
representing the current state of the program execution. Given a ranking function and choicefunctions, their appropriateness can be ensured by solving the safety verification of a program.
We give an example of appropriate choice functions and a ranking function for the program of
Figure 1c with specification 𝑆 1 (𝑥, 𝑦) = (𝑥 ≥ 0 ⇒ 𝑦 ≥ 0). Representing a state of the program as atuple of current values of 𝑎, 𝑏, 𝑠 and 𝑖, an example of appropriate choice functions is given by(true if 𝑎 = 𝑖 ∧ 𝑠 ≥ 0
choice3 (𝑎, 𝑏, 𝑠, 𝑖) = 𝑏
choice5 (𝑎, 𝑏, 𝑠, 𝑖) =false if 𝑎 ≠ 𝑖 ∨ 𝑠 < 0.
(true if 𝑎 ≤ 𝑖choice4 (𝑎, 𝑏, 𝑠, 𝑖) =false if 𝑎 > 𝑖
The program obtained by replacing rand𝑖∃ () with choice𝑖 (a,b,s,i) is shown in Figure 2. Under
the choice above, the program first executes i = i + 1 until i becomes a, then it executes s = s +f(i) where f(i) returns b, and then exits the loop. Then s = b < 0 (provided that the assertion
assert(a >= 0 and b < 0) is passed) and hence the assertion assert(s >= 0) fails as expected.
A ranking function is a witness of the fact that the chosen execution trace eventually breaks theloop: in this example, the number of the loop iteration is bounded by a+1.
Comparison with Other Methods
Albarghouthi et al. [2016] proposed a method for the maximal specification inference problem.
Their method uses a solver of the multi-abduction problem developed in the same paper.
The multi-abduction problem coincides with the maximal specification inference problem forloop-free programs. An important feature of the multi-abduction problem is that the maximality
checking of a candidate solution is reducible to SMT of quantified formulas. This fact can be
explained from the view point of program analysis as follows: a loop-free program has a simple
control flow, so its execution can be directly described by a first-order formula, where 𝑥 = rand∀ ()and 𝑦 = rand ∃ () are replaced with ∀𝑥 and ∃𝑦, respectively. Ranking function is needless because
the termination of a loop-free program is trivial.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:6

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

The method for the maximal specification inference in Albarghouthi et al. [2016] tries to prove
the reachability of a complex program by finding an under-approximation that reaches the assertion
failure. The class of under-approximations that they used consists of loop-free programs, which
can be obtained by expanding a loop an appropriate number of times and pruning branches thatseem unnecessary. Their method avoids the need of a ranking function by focusing on underapproximations that obviously terminate.
Unfortunately this approach has a limitation: there exists a program that the method of Albarghouthi et al. [2016] cannot find any maximal specification. Consider the maximal specification
inference problem for the program in Figure 1a. This program has a unique maximal specification, namely 𝑆 (𝑥, 𝑦) :⇔ (𝑥 ≥ 0 ⇒ 𝑦 ≥ 0). With this specification 𝑆, the program with angelic
and demonic branches in Figure 1c reaches the assertion failure. However none of its loop-freeunder-approximation reaches the assertion failure, i.e. for every loop-free under-approximation of
the program in Figure 1c, the daemon has appropriate choices for the values of rand∀ () so that the
program will not reach the assertion failure. The point is that every loop-free program has a bound𝑛 such that the program terminates within 𝑛 steps. Given an under-approximation of the programin Figure 1c, the daemon chooses a number greater than the bound 𝑛 as the value for a. Then f(a)is not called in the under-approximation, and hence the under-approximation cannot distinguishbetween 𝑆 and 𝑆 a,b .
From the view-point of the termination analysis, the method of Albarghouthi et al. [2016] tries
to find a ranking function independent of the daemon’s choice (a,b). However, all appropriate
ranking functions for Figure 1c depend on (a,b). So a more elaborated termination argument isinevitable in some cases.
Our method employs techniques of the termination analysis and actually find the maximal
solution for the program in Figure 1a.
The termination analysis of a program is a quite hard problem, and one may wonder if the
maximality checking problem is reducible to an easier problem such as SMT, which is decidable forsome theories. Prabhu et al. [2021] proposed a reduction of the maximality checking (of the CHC
optimization problem, which generalizes the maximal specification inference) to SMT, but we foundthat their algorithm is incorrect: The algorithm may erroneously judge a non-maximal solution
as maximal. We show that the maximality checking is as hard as the termination analysis4 of aTuring-complete programming language (Theorem 4.2), and hence it is not reducible to decidable
SMT. Actually this is the starting point of our work and the reason why we thought that thetermination analysis would be useful to the maximality checking.
3

THE PROBLEMS AND CLASSIFICATIONThis section briefly explains the optimization problems studied in this paper and compare themwith problems discussed in other work [Albarghouthi et al. 2016; Hashimoto and Unno 2015; Prabhu
et al. 2021; Zhou et al. 2021]. We assume the basic knowledge of first-order logic (see, e.g., Smullyan[1968]).
3.1

Preliminaries: Underlying Logics, Structures and Constraint Horn Clauses

The optimization problems are parameterized by first-order signatures. It consists of sets of (basic)
sorts, function symbols and predicate symbols. Each sort basically corresponds to a data type of thetarget programs: for example, if the target program uses integers and integer lists, the signature
4 Here the termination analysis means the problem to ask if a given program terminates on all inputs. This differs from (andis strictly harder than) the halting problem of Turing machines, which coincides with the problem to ask if a given program
terminates on a given input.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:7

has sorts int and int_list of integers and integer lists. Each symbol is sorted: a function symbol
is associated to its sort 𝑠 1 × · · · × 𝑠𝑛 → 𝑠, where 𝑠 1, . . . , 𝑠𝑛 , 𝑠 are basic sorts, and a predicate symbol
to 𝑠 1 × · · · × 𝑠𝑛 → Prop.
Example 3.1. The signature for linear integer arithmetic has unique sort int of integers, function
symbols + : int × int → int and 0, 1 : int, and a predicate symbol < : int × int → Prop.
We sometimes consider the signature with a function symbol ((−) mod 𝑛) : int → int for each
non-zero natural number 𝑛.
□
Given a signature, the set of formulas is defined as usual. A formula may have predicate variables
and/or function variables (in addition to predicate and function symbols specified in the signature).
In order to distinguish predicate/function variables from standard variables of first order logic, thelatter are sometimes called object variables. Object, predicate and function variables are sorted andonly well-sorted terms and formulas are considered in the sequel. A sentence is a closed formula,i.e. a formula with no free variable. A theory is a set of sentences.
The top-level universal quantifier
is often omitted: for example, ∀𝑥, 𝑦. 𝜑 (𝑥, 𝑦) ⇒ ∃𝑧.𝜓 (𝑥, 𝑦, 𝑧) is written as 𝜑 (𝑥, 𝑦) ⇒ ∃𝑧.𝜓 (𝑥, 𝑦, 𝑧).
A structure A determines the interpretation of each symbol. For each (basic) sort 𝑠, AJ𝑠K is a set;
For each function symbols 𝑓 of sort 𝑠 1 × · · · × 𝑠𝑛 → 𝑠, AJ𝑓 K is a function from AJ𝑠 1 K × · · · × AJ𝑠𝑛 K
to AJ𝑠K; For each predicate symbol 𝑃 of sort 𝑠 1 × · · · × 𝑠𝑛 → Prop, AJ𝑃K is a function from
AJ𝑠 1 K × · · · × AJ𝑠𝑛 K to the set of truth values {⊥, ⊤}. A structure determines the truth value ofeach sentence. The theory consisting of true sentences w.r.t. A is written as Th(A).
Example 3.2. The structure Z interprets each symbol in the signature of linear integer arithmetic
as expected: for example, int is interpreted as the set of integers Z. The theory of linear integer
arithmetic is Th(Z).
□Let us fix a first-order signature and its structure.
A constraint language is just a set of formulas (with no function/predicate variable).
Example 3.3. LIA is a constraint language consisting of all formulas of the signature of linear
integer arithmetic. OF-LIA consists of quantifier-free formulas of the signature of linear integer
arithmetic.
□
Let us fix a constraint language.
A constrained Horn clause (or CHC) is a formula of one of the following forms∀®
𝑥.

𝑃1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ 𝑄 (𝑢)
®

∀®
𝑥.

𝑃1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 =⇒ ⊥,where 𝑥® is the sequence of object variables appearing in the formula, 𝑡®1, . . . , 𝑡®𝑛 and 𝑢® are sequencesof terms, 𝜑 is a formula in the constraint language, and 𝑃1, . . . , 𝑃𝑛 and 𝑄 are predicate variables.
We assume that a CHC has no function variable.5 The position of 𝑄 is called the head position.
A CHC system is a finite set of CHCs, regarded as their conjunction. A formula that is logicallyequivalent to a conjunction of CHCs is sometimes called a CHC even if it is not a CHC in the proper
sense. An example of such a formula is ∀®
𝑥 . 𝑃 (𝑡®) ∧ 𝜑 =⇒ 𝑄 1 (𝑢®1 ) ∧ 𝑄 2 (𝑢®2 ), which is equivalent tothe conjunction of ∀®
𝑥 . 𝑃 (𝑡®) ∧ 𝜑 =⇒ 𝑄 1 (𝑢®1 ) and ∀®
𝑥 . 𝑃 (𝑡®) ∧ 𝜑 =⇒ 𝑄 2 (𝑢®2 ).
A solution of a CHC system is an interpretation of predicate variables that makes all formulas in
the system true. For a solution 𝜉, we write 𝜉 (𝑃) for the interpretation of 𝑃 under 𝜉. The solutions
are naturally ordered: 𝜉 ≤ 𝜁 if and only if ∀®
𝑥 .𝜉 (𝑃) (𝑥)® =⇒ 𝜁 (𝑃) (𝑥)® for every predicate variable 𝑃.
The problem to decide if a given CHC system has a solution is called the CHC satisfiability problem.
5 Formulas with function variables shall be used in Sections 5 and 6.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:8

3.2

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

CHC Optimization

Now we define the CHC optimization problem.
Definition 3.4 (CHC optimization [Hashimoto and Unno 2015]). For interpretations 𝜉 and 𝜁 ofpredicate variables PV = {𝑃 1, . . . , 𝑃𝑛 } and a subset X ⊆ PV , we write 𝜉 < X 𝜁 if ∀®
𝑥 .𝜉 (𝑃) (𝑥)® ⇒𝜁 (𝑃) (𝑥)® for every 𝑃 ∈ X and the implication is proper for some 𝑃 ∈ X. The CHC optimization is aproblem of one of the following forms:
maximize X s.t. C

minimize X s.t. C

where C is a CHC system and X is a subset of predicate variables in C. In the former case, the goal
is to find a maximal solution 𝜉 of C w.r.t. < X , i.e. a solution 𝜉 such that there is no solution 𝜁 of C
satisfying 𝜉 < X 𝜁 . In the latter case, the goal is to find a minimal solution w.r.t. < X .
□Remark 1. Note that the CHC optimization problem asks to find a solution that is maximal/minimal
among all semantic solutions. As we shall see, our procedure tries to construct a logical formula
representing a maximal/minimal solution. Hence our goal is to find a syntactic solution that issemantically maximal/minimal.
Other settings can be found in the literature. For example, one may want to find a syntactic
solution that is maximal/minimal among those expressive in a certain class of formulas [Hashimotoand Unno 2015; Srivastava and Gulwani 2009; Zhou et al. 2021]. Examples of such classes offormulas include the set of formulas shorter than a certain bound [Hashimoto and Unno 2015; Zhou
et al. 2021] and the set of conjunctions of a certain finite set of formulas [Srivastava and Gulwani2009].
□
Remark 2. One may be interested in a more complicated optimization problem likemaximize X minimize Y maximize Z s.t. C,
where X, Y and Z are disjoint sets of predicate variables in C. This requires to find a solution thatis maximal in X and Z and minimal in Y, where X is more significant (i.e., if 𝜉 < X 𝜁 and 𝜉 < Y 𝜁 ,then 𝜁 is more desirable). This problem can be solved by iteratively solving the CHC optimization
problem. First solve maximize X s.t. C and let 𝜉 be a maximal solution w.r.t. < X . Our procedure
returns a formula 𝜉 (𝑃) for each 𝑃 ∈ X. Let C ′ be the CHC system obtained by replacing 𝑃 ∈ X in
C with 𝜉 (𝑃). Then it suffices to solve the subproblem minimize Y maximize Z s.t. C ′.
□Some subproblems are studied in other papers [Albarghouthi et al. 2016; Prabhu et al. 2021; Zhou
et al. 2021].
• Linear multi-abduction [Albarghouthi et al. 2016]: This is a problem to find a maximal
solution of∀®
𝑥 . 𝑃 1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 ⇒ ⊥,where 𝑃1, . . . , 𝑃𝑛 are distinct predicate variables.
• (Non-linear) multi-abduction [Albarghouthi et al. 2016]: This is a problem to find a maximal solution of∀®
𝑥 . 𝑃 1 (𝑡®1 ) ∧ · · · ∧ 𝑃𝑛 (𝑡®𝑛 ) ∧ 𝜑 ⇒ ⊥.
Here a predicate variable can appear more than once.
• open CHC optimization: This is a problem of the form maximize X s.t. C, where C
is a CHC system that is open w.r.t. X. Here a CHC system is open w.r.t. X if, for every
𝑃 ∈ X, 𝑃 has no head occurrence in C. This problem coincides with maximal specification
inference [Albarghouthi et al. 2016].
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:9

Among them, linear multi-abduction is easiest and CHC optimization is hardest.
From the view point of specification inference, open CHC optimization corresponds to theinference of the maximal specification of an external function f: the caller of f together withassertions is given but the implementation of f is not. The CHC optimization problem coincides
with a variant of the maximal specification inference problem, where both the caller of f and theimplementation of f are given.
4

THEORETICAL ANALYSIS OF CHC OPTIMIZATIONThis section analyzes the CHC optimization problem from a theoretical view point.
The theoretical analysis of this section is motivated by an incorrect reduction of the maximality
checking of a given solution of CHCs to SMT solving proposed by Prabhu et al. [2021]. As shownby Albarghouthi et al. [2016], the reduction is correct for the multi-abduction problem but, as weshall see, it does not work for the CHC optimization. So it is natural to ask if it is possible to reducethe maximality checking of the CHC optimization problem to SMT.
We show that the maximality checking of the CHC optimization problem is Π 02 -complete (Theorem 4.2). This result gives a negative answer to the above question: the maximality checking
is undecidable and hence is not reducible to a decidable SMT. Theorem 4.2 also has a positive
consequence: techniques to solve any Π 02 -hard problem would be applicable to the maximality
checking. Motivated by this observation, we shall discuss in the next section how one can apply
techniques for the termination analysis of programs, which is a typical Π 02 -complete problem, tothe maximality checking.
This section also discusses the existence of a maximal solution.
4.1

Motivation: Maximality Checking and SMT Solving

The maximality problem for multi-abduction can be reduced to (quantified) SMT, as shown by
Albarghouthi et al. [2016], and hence the maximality problem for multi-abduction over QF-LIA isdecidable. It is natural to ask if the maximality checking for CHC optimization is also reducible to
SMT solving, and actually an attempt can be found in the literature [Prabhu et al. 2021]. In thissubsection, we briefly review the maximality-checking algorithm for multi-abduction [Albarghouthi
et al. 2016] and a subtlety of CHC optimization.
The key property of multi-abduction problem is the downward-closedness of solutions: if 𝜁 is asolution and 𝜉 ≤ 𝜁 , then 𝜉 is also a solution. This allows us to reduce the maximality checking to
SMT, as we shall see. Consider the following multi-abduction problem:∀𝑥, 𝑦.

𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜑 (𝑥, 𝑦) ⇒ ⊥and let 𝜉 be a non-maximal solution, i.e. 𝜉 < 𝜁 for some solution 𝜁 . The shape of 𝜁 (𝑃) is unclear. A
trick is to choose an element 𝑐 in the difference between 𝜉 (𝑃) and 𝜁 (𝑃) and to consider 𝜁 ′ (𝑃) (𝑥) :=(𝜉 (𝑃) (𝑥) ∨ 𝑥 = 𝑐). Then 𝜉 < 𝜁 ′ ≤ 𝜁 and, by the downward-closedness of solutions, 𝜁 ′ is also asolution. Hence, if 𝜉 is not maximal, there exists a solution 𝜁 ′ such that 𝜁 ′ (𝑃) (𝑥) = (𝜉 (𝑃) (𝑥) ∨𝑥 = 𝑐)for some 𝑐 with ¬𝜉 (𝑃) (𝑐). The existence of such a solution can be reduced to (quantified) SMT,
namely the validity of∃𝑐. ¬𝜓 (𝑐) ∧ ∀𝑥, 𝑦. (𝜓 (𝑥) ∨ 𝑥 = 𝑐) ∧ (𝜓 (𝑦) ∨ 𝑦 = 𝑐) ∧ 𝜑 (𝑥, 𝑦) ⇒ ⊥where 𝜓 (𝑥) := 𝜉 (𝑃) (𝑥).
This approach based on the one-point extension of the current solution does not work for CHC
systems. For example, consider the following CHC system over LIA∀𝑥, 𝑦.

𝑃 (𝑥) ∧ (𝑥 mod 2 = 𝑦 mod 2) ⇒ 𝑃 (𝑦)Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:10Yu Gu, Takeshi Tsukada, and Hiroshi Unno

and a solution 𝜉 (𝑃) (𝑥) = (𝑥 mod 2 = 0). The unique maximal solution is 𝜁 (𝑃) (𝑥) = ⊤ and thus
𝜉 is not maximal. However there is no solution of the form 𝜁 ′ (𝑃) (𝑥) = (𝜉 (𝑃) (𝑥) ∨ 𝑥 = 𝑐) for any
constant 𝑐 such that ¬𝜉 (𝑃) (𝑐); to extend 𝜉, one needs to add more than one points.
The maximality problem for CHC optimization was studied in [Prabhu et al. 2021]. They proposedan algorithm for checking the maximality that reduces the maximality problem to SMT, based on
the above-discussed idea of one-point extension [Prabhu et al. 2021, Algorithm 6 and Theorem 5.2].
We found that their algorithm is incorrect by the reason discussed above:6 The algorithm mayerroneously judge a non-maximal solution as maximal.
It is natural to ask if the maximality problem for CHCs is reducible to SMT, despite the essential
difference between multi-abduction and CHC optimization. The theoretical analysis in the next
subsection gives an answer.
4.2

Undecidability of Maximality Checking

Let us first formally define the maximality checking problem.
Definition 4.1. The maximality checking problem asks if, given a CHC system C over predicate
variables PV = {𝑃1, . . . , 𝑃𝑛 }, a subset X ⊆ PV of predicate variables and a syntactic representationof a solution 𝜉 (i.e. a formula 𝜉 (𝑃) in the constraint language for each predicate variable 𝑃 ∈ PV ),there exists a solution 𝜁 such that 𝜉 < X 𝜁 . Note that 𝜉 must be definable in the constraint language
whereas 𝜁 is not necessarily so.7□
The next theorem shows the hardness of the maximality problem for CHCs over QF-LIA, acommonly used constraint language.
Theorem 4.2. The maximality problem for (open) CHCs over QF-LIA is Π 02 -complete.
Proof. We prove (1) the maximality checking problem for open CHCs is Π 02 -hard and (2) the
maximality checking problem for CHCs is in Π 02 . Since the maximality checking problem for open
CHCs is a subproblem of the problem for CHCs, the theorem follows from these claims.
(1) We reduce the validity problem for Π 02 formulas, which is Π 02 -complete, to the maximality
problem. The validity problem for Π02 formulas asks if ∀𝑥 .∃𝑦.𝑃 (𝑥, 𝑦) is true for a given computablepredicate 𝑃 (𝑥, 𝑦) over integers 𝑥, 𝑦. Given a computable predicate 𝑃, consider the following programwith an external function f:
i = f(); j = 0;
while (not P(i,j)) and (not P(i,-j)) doj = j + 1;
assert(false);(here P(i,j) is a procedure that calculates 𝑃 (𝑖, 𝑗), which is computable by assumption). The
candidate specification for f is ⊥, which is trivially sound. The specification ⊥ is maximal if andonly if the program fails whatever f returns. The latter condition is equivalent to ∀𝑥 .∃𝑦.𝑃 (𝑥, 𝑦) as
required.
By the standard translation of programs to CHCs, we obtain a CHC system C representing
the above program. Note that the multiplication is definable by a program only using +, ≤, 0 and
1, the resulting CHCs do not need to contain the multiplication symbol. Let 𝐹 be the predicate
symbol corresponding to f. It suffices to find a solution 𝜉 of C that is definable by the constraint
6 We contacted the authors of the paper [Prabhu et al. 2021] and they confirmed that the proof of the correctness theorem[Prabhu et al. 2021, Theorem 5.2] of their maximality checking algorithm isMaximal [Prabhu et al. 2021, Algorithm 6] waswrong.
7 A solution 𝜉 obtained by a CHC solver usually satisfies this condition. The comparator 𝜁 should be unrestricted since weare interested in maximality in the semantic domain.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:11

language and satisfies 𝜉 (𝐹 ) = ⊥. We consider a slight modification C ′ of C: for each Horn clause(∀®
𝑥 .Φ ⇒ Ψ) ∈ C, C ′ has its variant ∀®
𝑥𝑦.Φ ∧ 𝐹 (𝑦) ⇒ Ψ where 𝑦 is a fresh variable not in 𝑥.
® Then′C is essentially the same as C if the assignment for 𝐹 is not empty, but all clauses in C ′ is “disabled”
if 𝐹 is empty. Then the assignment 𝜉 that maps every predicate variable 𝑄 ∈ PV to ⊥ is a solutionof C ′, and ∀𝑥 .∃𝑦.𝑃 (𝑥, 𝑦) is true if and only if the solution 𝜉 is a maximal solution of C ′ with respectto < {𝐹 } .
(2) Let C be a CHC, X = {𝑃1, . . . , 𝑃𝑛 } be a chosen subset of predicate variables and 𝜉 be a
candidate solution for C. Let 𝜑𝑖 := 𝜉 (𝑃𝑖 ). Then 𝜉 is maximal w.r.t. X if and only if
C ∪ { 𝜑 (𝑥®𝑖 ) ⇒ 𝑃𝑖 (𝑥®𝑖 ) | 𝑖 = 1, . . . , 𝑛 } ∪ {⊤ ⇒ 𝑃𝑖 (®
𝑐𝑖 ) | 𝑖 = 1, . . . , 𝑛}is unsatisfiable for every 𝑐® := (®
𝑐𝑖 )𝑖=1,...,𝑛 such that |= ¬𝜑 1 (®
𝑐 1 ) ∨ · · · ∨ ¬𝜑𝑛 (®
𝑐𝑛 ). It is well-known thatthe unsatisfiability of CHCs over LIA is in Σ01 ; hence there exists a computable predicate Ψ suchthat the above CHC system is unsatisfiable if and only if |= ∃𝑦.Ψ(®
𝑐 , 𝑦). So 𝜉 is maximal w.r.t. < X if
and only if |= ∀®
𝑐 .∃𝑦.(𝜑 1 (®
𝑐 1 ) ∧ · · · ∧ 𝜑𝑛 (®
𝑐𝑛 )) ∨ Ψ(®
𝑐 , 𝑦). So the maximality problem belongs to Π 02 . □This result has both positive and negative consequences.
On the negative side, it shows that the maximality problem cannot be completely solved by any
decision procedures, including SMT, no matter how cleverly it is reduced.
Corollary 4.3. Both the maximality problem and the non-maximality problem for (open) CHCs
over QF-LIA are undecidable.
□
On the positive side, it suggests that an approach to a Π 02 -complete problem would be applicableto the maximality problem. Section 5 discusses an approach to the maximality/minimality checking
inspired by Theorem 4.2.
4.3

Existence of an Optimal Solution

Let us first examine the existence of a maximal/minimal solution in the semantic domain. It is wellknown that a satisfiable CHC system has the minimum solution. Although it does not necessarily
have the maximum solution, it always has a maximal solution.
Theorem 4.4. Every satisfiable CHC system has a maximal solution.
Proof. Let C be a CHC system over predicate variables PV , X ⊆ PV and S be the set of all
solution of C. The solutions are ordered by 𝜁 ≤ X 𝜉 :⇔ (∀𝑃 ∈ X.𝜁 (𝑃) ⇒ 𝜉 (𝑃)).
First we prove the claim for the case X = PV . We use Zorn’s lemma. To apply Zorn’s lemma, itsuffices to show that, for every linearly ordered subset L ⊆ S, there exists a solution 𝜁 ∈ S suchÔthat ∀𝜉 ∈ L. 𝜉 ≤PV 𝜁 . Given a linearly ordered subset L ⊆ S, we define 𝜁 by 𝜁 (𝑃) := 𝜉 ∈L 𝜉 (𝑃).
Obviously ∀𝜉 ∈ L. 𝜉 ≤PV 𝜁 , and it is not difficult to check that 𝜉 is a solution of C. So we can apply
Zorn’s lemma, concluding that S has a maximal element w.r.t. ≤PV .
Let us consider the general case. For a solution 𝜉, we write 𝜉ˆ for the solution that coincides with
𝜉 on X and 𝜉ˆ(𝑄) = min{𝜁 (𝑄) | 𝜁 ∈ S ∧ ∀𝑃 ∈ X.𝜁 (𝑃) = 𝜉 (𝑃)} for 𝑄 ∉ X. The right-hand-side is
well-defined since every satisfiable CHC system has the minimum solution. Then 𝜉 ≤ X 𝜁 if andonly if 𝜉ˆ ≤PV 𝜁ˆ. Given a linearly ordered subset L ⊆ S w.r.t. ≤ X , the set L̂ := {𝜉ˆ | 𝜉 ∈ L} is alinearly ordered subset w.r.t. ≤PV . We can apply the above argument to L̂ to construct an upperbound of L w.r.t. ≤ X .
□A more interesting question is whether there exists a maximal solution with a syntactic representation, since a solver of the CHC optimization problem is usually expected to output a
maximal/minimal solution. Albarghouthi et al. [2016, Theorem 5] gave a negative result for thetheory of linear real arithmetic (LRA).
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:12

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

Theorem 4.5 ([Albarghouthi et al. 2016, Theorem 5]). The multi-abduction problem over LRA
may not have a maximal solution in LRA.
□
We show that this is also the case for LIA.
Proposition 4.6. The multi-abduction problem
𝑃 (𝑥, 𝑦) ∧ 𝑃 (𝑥 + 𝑦, 𝑦) =⇒ ⊥over LIA does not have a maximal solution in LIA (even with the mod operators).
Proof. (Sketch) Assume for contradiction that there is a maximal solution 𝜑 (𝑥, 𝑦) in LIA. Since
LIA with the modulo operators ((−) mod 𝑛) (𝑛 > 1 is a constant) admits quantifier elimination, we
can assume without loss of generality that 𝜑 (𝑥, 𝑦) is quantifier-free. Let 𝑛 be a common multiplierof {𝑚 ∈ N | (𝑒 mod 𝑚) appears in 𝜑 }. Then 𝜑 can be transformed into the following from:𝜑 (𝑥, 𝑦)⇔𝑁Ü𝜓𝑖 (𝑥, 𝑦)𝑖=1

where 𝜓𝑖 (𝑥, 𝑦) is(𝑥 mod 𝑛 = 𝑐𝑖′) ∧ (𝑦 mod 𝑛 = 𝑐𝑖′′) ∧𝑀𝑖Û𝑎𝑖,𝑗 𝑥 + 𝑏𝑖,𝑗 𝑦 + 𝑐𝑖,𝑗 ≥ 0

𝑗=1

for each 𝑖. An important property of 𝜓𝑖 is that, if 𝜓𝑖 (𝑚, 𝑛) and 𝜓𝑖 (𝑚 + 𝑘𝑛, 𝑛) hold, then 𝜓𝑖 (𝑚 + 𝑘 ′𝑛, 𝑛)
holds for every 0 ≤ 𝑘 ′ ≤ 𝑘.
Since 𝜑 is a maximal solution, at least one of 𝜑 (𝑚, 𝑛), 𝜑 (𝑚 + 𝑛, 𝑛), 𝜑 (𝑚 + 2𝑛, 𝑛) must be truefor every 𝑚; otherwise 𝜑 ∨ (𝑥 = 𝑚 + 𝑛 ∧ 𝑦 = 𝑛) is a solution which is strictly greater than 𝜑.
Hence at least 𝑁 + 1 points from (0, 𝑛), (𝑛, 𝑛), (2𝑛, 𝑛), . . . , ((3𝑁 + 3)𝑛, 𝑛) must satisfy 𝜑. By the
pigeonhole principle, there exists 𝑖 such that 𝜓𝑖 is true at least two distinct points in the above list,say (𝑚𝑛, 𝑛) and (𝑚 ′𝑛, 𝑛), 𝑚 < 𝑚 ′. Then 𝜓𝑖 ((𝑚 + 1)𝑛, 𝑛) also holds because of the above discussed
property of 𝜓𝑖 . Hence both 𝜑 (𝑚𝑛, 𝑛) and 𝜑 ((𝑚 + 1)𝑛, 𝑛) is true and thus 𝜑 violates the constraint, acontradiction.
□
5

MAXIMALITY AS TERMINATIONThis section discusses our approach to the maximality problem using the termination analysis ofprograms. This approach is motivated by the theoretical analysis in the previous section: we haveseen that the maximality problem is Π02 -complete and the termination analysis8 is a well-knownΠ 02 -complete problem.
Main results of this section are reductions of the (non)optimality9 of a given solution to constraint
satisfaction problems that extends the CHC satisfiability problem:• The non-minimality and non-maximality problems are reduced to the satisfiability problemof CHCs with non-emptiness constraints.
8 The termination analysis here asks if a given program terminates on all inputs. The termination analysis in this sense isstrictly harder than the halting problem, which asks if a given program terminates on a given input.
9 We shall discuss reductions of both the optimality checking and the non-optimality checking, giving a constraint set
that is satisfiable when a given solution is optimal, as well as a constraint set that is satisfiable when the given solution
is not optimal. One may find it redundant since the satisfiability of the latter is equivalent to the unsatisfiability of theformer. It is, however, not redundant because of the asymmetry between satisfiability and unsatisfiability: although thesatisfiability of a constraint set is witnessed by a solution, it is usually hard to ensure that a constraint set is unsatisfiable. In
our implementation, to decide whether a given solution is optimal or not, we run two constraint solvers in parallel, one ofwhich solves the constraint corresponding to the optimality checking and the other to the non-optimality.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:13• The minimality and maximality problems are reduced to the satisfiability problem of CHCs
with function variables and well-foundedness predicate.
The latter is based on the idea of the termination analysis of programs, illustrated in Section 2.
Here the well-foundedness predicate comes from the termination analysis.
For simplicity, this section studies the following CHC system with a single predicate variable 𝑃∀𝑥 . 𝜄 (𝑥) =⇒ 𝑃 (𝑥)∀𝑥, 𝑦, 𝑧.

∀𝑥 .

𝑃 (𝑥) =⇒ 𝜎 (𝑥)𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧).

(1)

We also assume a solution 𝜗 of the above system.
5.1

Non-Optimality and CHC with Non-EmptinessThis subsection discusses a way to find a better solution, under the assumption that the solution 𝜗
is not optimal. The non-optimality checking can be easily reduced to the satisfiability problem for
CHCs with non-emptiness, i.e. a system of CHCs with non-emptiness constraint 𝑃 ≠ ∅ for somepredicate variables 𝑃.
The candidate solution 𝜗 is non-maximal if and only if the following CHC system with nonemptiness is satisfiable:
𝑄≠∅∀𝑥 . 𝜗 (𝑥) ∧ 𝑄 (𝑥) =⇒ ⊥∀𝑥 . 𝑄 (𝑥) =⇒ 𝑃 (𝑥)∀𝑥 . 𝜗 (𝑥) =⇒ 𝑃 (𝑥)∀𝑥 . 𝑃 (𝑥) =⇒ 𝜎 (𝑥)∀𝑥, 𝑦, 𝑧. 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧).
Suppose that 𝜗 is not maximal, i.e. there exists another solution 𝜗 ′ such that ∀𝑥 .(𝜗 (𝑥) =⇒ 𝜗 ′ (𝑥))and ∃𝑥 .(¬𝜗 (𝑥) ∧ 𝜗 ′ (𝑥)). Then the substitution given by 𝑃 ↦→ 𝜗 ′ and 𝑄 ↦→ ¬𝜗 ∧ 𝜗 ′ is a solution of
the above system. Conversely, if the above system is satisfiable, the assignment to 𝑃 by a solution isstrictly larger than 𝜗, since 𝑄 is non-empty and disjoint with 𝜗 and 𝑃 contains both 𝑄 and 𝜗. Since𝜄 (𝑥) =⇒ 𝜗 (𝑥), the assignment to 𝑃 by the solution satisfies the CHC system (1).
The non-minimality checking problem can be solved by a similar way. The candidate solution 𝜗
is non-minimal if and only if the following system is satisfiable:
𝑄≠∅∀𝑥 . 𝑄 (𝑥) =⇒ 𝜗 (𝑥)∀𝑥 . 𝜄 (𝑥) =⇒ 𝑃 (𝑥)∀𝑥 . 𝑃 (𝑥) ∧ 𝑄 (𝑥) =⇒ ⊥∀𝑥 . 𝑃 (𝑥) =⇒ 𝜗 (𝑥)∀𝑥, 𝑦, 𝑧. 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧).
If 𝜗 is not minimal, there exists another solution 𝜗 ′ of (1) such that ∀𝑥 .(𝜗 ′ (𝑥) =⇒ 𝜗 (𝑥)) and∃𝑥 .(¬𝜗 ′ (𝑥) ∧ 𝜗 (𝑥)). Then the assignment given by 𝑃 ↦→ 𝜗 ′ and 𝑄 ↦→ 𝜗 ∧ ¬𝜗 ′ is a solution of
the above constraints. Conversely, if the above constraints are satisfiable, then the value of 𝑃 in
the solution is a strictly smaller solution of (1). Actually 𝑃 (𝑥) =⇒ 𝜗 (𝑥) requires 𝑃 to be smaller
than or equal to 𝜗. Furthermore, since 𝑄 must contain an element satisfying 𝜗, the constraint
𝑃 (𝑥) ∧ 𝑄 (𝑥) =⇒ ⊥ requires that 𝑃 is strictly smaller than 𝜗.
Example 5.1. Consider the following system of CHCs
𝑃 (1),∀𝑥, 𝑦. 𝑃 (𝑥) ∧ 𝑃 (𝑦) =⇒ 𝑃 (𝑥 + 𝑦)

and its solution 𝜗 (𝑥) = ⊤, which is not minimum. The system of CHCs with non-emptiness for the
non-minimality checking is given by𝑄≠∅∀𝑥 . 𝑄 (𝑥) =⇒ ⊤𝑃 (1)∀𝑥 . 𝑃 (𝑥) ∧ 𝑄 (𝑥) =⇒ ⊥∀𝑥 . 𝑃 (𝑥) =⇒ ⊤.

∀𝑥, 𝑦, 𝑧. 𝑃 (𝑥) ∧ 𝑃 (𝑦) =⇒ 𝑃 (𝑥 + 𝑦)
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:14

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

A solution is 𝑄 (𝑥) = (−3 ≤ 𝑥 ≤ −1) and 𝑃 (𝑥) = (𝑥 ≥ 0).

□

For a satisfiable system of CHCs with non-emptiness constraint, the construction of a solutionof the system is not harder than the standard CHC solving, at least in theory. This would be
surprising since the satisfiability checking for this kind of systems is quite hard (i.e. Π 02 -complete).
The procedure for generating a solution simply enumerates the elements 𝑐 of the domain D andtries to construct a solution of the CHC system obtained by replacing 𝑄 ≠ ∅ with 𝑄 (𝑐). Since thesystem is assumed to be satisfiable, the procedure eventually finds an appropriate element 𝑐ˆ andgives a solution. This gives an algorithm using the CHC solver as an oracle.
In Section 6.4, we shall discuss a solver of CHCs with non-emptiness that basically follows theabove-mentioned idea. A key to effectively solve the problems is a heuristic to choose an appropriateelement 𝑐 that one expects to be contained in a non-empty predicate 𝑄.
Remark 3. As shown by Albarghouthi et al. [2016], the checking of non-optimality of a multiabduction can be reduced to SMT (of formulas with both existential and universal quantifiers).
Theorem 4.2 shows that the maximality problem for open CHCs (which coincides with the maximal
specification inference in [Albarghouthi et al. 2016]) cannot be reduced to SMT. Note that the SMT
over LIA is decidable but the maximality problem for open CHCs is Π 02 -complete, which is strictly
harder than any decidable problems (and even than the halting problem).
□
5.2

Minimality Checking as Termination

Let us consider the case that the candidate solution 𝜗 is minimal. We discuss a way to show that itis actually minimal.
It is well-known that every satisfiable CHC system has the minimum solution. More precisely,
the subset of constraints∀𝑥 .

𝜄 (𝑥) =⇒ 𝑃 (𝑥)∀𝑥, 𝑦, 𝑧.

𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧)ˆ and the CHC system is satisfiable if and only if |= 𝜗ˆ (𝑥) =⇒ 𝜎 (𝑥);has the minimum solution 𝜗,
hence 𝜗ˆ is the minimum solution of the CHC system (1) if it is satisfiable.
ˆ here we discuss a characterization
There are several characterizations of the minimum solution 𝜗;
by a proof system. Let D be the domain of 𝑥, 𝑦, 𝑧 in the CHC system (1). A judgement is of the form
𝑃 (𝑐), where 𝑐 ∈ D. The proof rules are:𝑃 (𝑐)[ |= 𝜄 (𝑐)]𝑃 (𝑑) 𝑃 (𝑑 ′)[ |= 𝜏 (𝑑, 𝑑 ′, 𝑐)]𝑃 (𝑐)where [] is the side condition needed to use the rule.
Proposition 5.2. 𝑃 (𝑐) is provable if and only if |= 𝜗ˆ (𝑐).
Proof. The left-to-right direction can be proved easily by induction on the structure of proofs.
To prove the converse, it suffices to show that {𝑐 ∈ D | 𝑃 (𝑐) is provable} is a solution, which isalso easy.
□
Therefore the candidate solution 𝜗 is minimum if and only if 𝑃 (𝑐) is provable for every 𝑐 ∈ Dsuch that |= 𝜗 (𝑐). The problem whether 𝑃 (𝑐) is provable is a kind of termination analysis, as weshall see below.
The termination problem considered here is concerned with transition systems with angelic
and demonic nondeterminism. The angelic branches are chosen so that the system satisfies a
required property; the demonic branches are chosen so that the system violates the property. The
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:15

angelic-demonic termination problem asks if, given a system with angelic and demonic branches, it
is possible to choose angelic branches so that the system terminates whatever demonic branches
are chosen.
We regard the goal-oriented proof search as the angelic-demonic termination problem.
• To construct a proof of 𝑃 (𝑐), one needs to choose a proof rule. When one chooses the right
rule, one also needs to choose premises 𝑃 (𝑑) and 𝑃 (𝑑 ′). These nondeterminismtic branches
are angelic, i.e. an appropriate rule and premises should be chosen.
• When the right-rule is chosen, one needs to proof the premises 𝑃 (𝑑) and 𝑃 (𝑑 ′) as well. Insteadof checking existence of proofs for all premises, the daemon chooses one premise whichshould be examined and we check the existence of a proof of the chosen premise. This choice
is implemented by demonic nondeterministic branching.
This system terminates from 𝑐 if and only if 𝑃 (𝑐) is provable.10 Hence 𝜗 is minimum if and only if
the system terminates from every state 𝑐 such that |= 𝜗 (𝑐).
We reformulate the termination analysis as a constraint solving. Observe that it suffices to choose
a proof rule for each 𝑐 such that |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐), since 𝑃 (𝑐) is trivially provable if 𝜄 (𝑐) holds. Let 𝑐be an element such that |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐). There is only one proof rule that concludes 𝑃 (𝑐), namely,
𝑃 (𝑑 1 )𝑃 (𝑑 2 )𝑃 (𝑐)where |= 𝜏 (𝑑 1, 𝑑 2, 𝑐).

If the choice is appropriate, the premises are provable, that means, 𝑑 1 and 𝑑 2 again belong to theminimum solution. As we have to choose 𝑑 1 and 𝑑 2 for each 𝑐, the choices induce two functions
defined by 𝑓1 (𝑐) = 𝑑 1 and 𝑓2 (𝑐) = 𝑑 2 (for each 𝑐 such that |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐)). Since |= 𝜏 (𝑑 1, 𝑑 2, 𝑐) must
hold and 𝑑 1 and 𝑑 2 must belong to the minimum solution, we have the following constraint forfunction symbols 𝑓1 and 𝑓2 :(𝜗 (𝑧) ∧ ¬𝜄 (𝑧)) ⇒ (𝜗 (𝑓1 (𝑧)) ∧ 𝜗 (𝑓2 (𝑧)) ∧ 𝜏 (𝑓1 (𝑧), 𝑓2 (𝑧), 𝑧)).
Furthermore 𝑔𝑛 (. . . 𝑔2 (𝑔1 (𝑐)) . . . ) eventually reaches a state satisfying 𝜄 for every choice of 𝑔𝑖 = 𝑓1
or 𝑓2 . This kind of constraint can be expressed by using the well-foundedness predicate WF: WF (𝑊 )is true if and only if there is no infinite sequence 𝑐 0, 𝑐 1, 𝑐 2, . . . , such that 𝑊 (𝑐𝑖 , 𝑐𝑖+1 ) for every 𝑖 ∈ N.
In this case, the above-mentioned requirement is the well-foundedness of the relation𝑊:={(𝑐, 𝑓1 (𝑐)) | |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐)} ∪ {(𝑐, 𝑓2 (𝑐)) | |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐)}.

Summarizing the above argument results in the following constraint set, where 𝑓1, 𝑓2 : D → D
and 𝑊 : D × D → Prop:
𝜗 (𝑓1 (𝑧)) ∧ 𝜗 (𝑓2 (𝑧)) ∧ 𝑊 (𝑧, 𝑓1 (𝑧))∧𝑊 (𝑧, 𝑓2 (𝑧)) ∧ 𝜏 (𝑓1 (𝑧), 𝑓2 (𝑧), 𝑧)
WF (𝑊 ).

∀𝑧. 𝜗 (𝑧) ∧ ¬𝜄 (𝑧) =⇒(2)

Theorem 5.3. 𝜗 is the minimum solution of (1) if and only if the constraint set (2) is satisfiable.
Proof. Suppose that 𝜗 is minimum. Then |= 𝜗 (𝑐) if and only if 𝑃 (𝑐) is provable. For each 𝑐 suchthat |= 𝜗 (𝑐) ∧ ¬𝜄 (𝑐), let 𝑟 (𝑐) be the size of the smallest proof of 𝑃 (𝑐). Choose a proof of 𝑃 (𝑐) of size𝑟 (𝑐). If the proof concludes 𝑃 (𝑐) from 𝑃 (𝑑) and 𝑃 (𝑑 ′), then 𝑓1 (𝑐) := 𝑑 and 𝑓2 (𝑐) := 𝑑 ′. Let 𝑊 be
the predicate defined by: 𝑊 (𝑐, 𝑐 ′) if and only if both 𝑃 (𝑐) and 𝑃 (𝑐 ′) are provable and 𝑟 (𝑐) > 𝑟 (𝑐 ′).
Then 𝑓1, 𝑓2,𝑊 satisfies the above constraint.
10 We omit the proof of this fact. Omitting the proof does not cause any logical problem, because this is used only to illustrate

the intuition behind the constraint set defined below, the correctness of which will be proved independently of the argument
here.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:16

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

To prove the converse, suppose that the above constraints are satisfiable. Let (𝑓1, 𝑓2,𝑊 ) be asolution. We construct a proof of 𝑃 (𝑐) for each 𝑐 such that |= 𝜗 (𝑐) by induction on 𝑊 . If |= 𝜄 (𝑐),then 𝑃 (𝑐) is trivially provable. If |= ¬𝜄 (𝑐), then 𝑓1 (𝑐) and 𝑓2 (𝑐) satisfy 𝜗 and are strictly smaller than𝑐 with respect to 𝑊 . Hence by the induction hypothesis, 𝑃 (𝑓1 (𝑐)) and 𝑃 (𝑓2 (𝑐)) are provable. Then
𝑃 (𝑐) is provable since |= 𝜏 (𝑓1 (𝑐), 𝑓2 (𝑐), 𝑐).
□Example 5.4. Consider the following system of CHCs:
𝑃 (1),∀𝑥, 𝑦. 𝑃 (𝑥) ∧ 𝑃 (𝑦) =⇒ 𝑃 (𝑥 + 𝑦).

Then the minimum solution is 𝑃 (𝑥) = (𝑥 ≥ 1). The constraints expressing the termination problem
is: WF (𝑊 ) and∀𝑧. 𝑧 > 1 =⇒𝑓1 (𝑧) ≥ 1 ∧ 𝑓2 (𝑧) ≥ 1 ∧ 𝑊 (𝑧, 𝑓1 (𝑧))∧ 𝑊 (𝑧, 𝑓2 (𝑧)) ∧ 𝑧 = 𝑓1 (𝑧) + 𝑓2 (𝑧).

A solution is 𝑓1 (𝑥) = 1, 𝑓2 (𝑥) = (𝑥 − 1), and 𝑊 (𝑥, 𝑦) = (𝑥 > 𝑦 ≥ 1).
5.3□

Maximality Checking as Termination

Suppose that the candidate solution 𝜗 of (1) is maximal. This subsection discusses how to prove themaximality of 𝜗.
Since 𝜗 is maximal, there is no solution 𝜗 ′ which is strictly greater than 𝜗. In particular, forevery 𝑐 such that |= ¬𝜗 (𝑐), there is no solution that subsumes 𝜗 (𝑥) ∨ (𝑥 = 𝑐). Hence the CHC
system obtained by replacing 𝜄 (𝑥) in (1) with 𝜗𝑐 (𝑥) := (𝜗 (𝑥) ∨ 𝑥 = 𝑐) is unsatisfiable, because
𝜄 in (1) is a lower bound of the solution. Therefore, for the minimum solution 𝜚 𝑐 of { 𝜗𝑐 (𝑥) =⇒𝑃 (𝑥), 𝑃 (𝑥) ∧ 𝑃 (𝑦) ∧ 𝜏 (𝑥, 𝑦, 𝑧) =⇒ 𝑃 (𝑧) }, we have |= ¬(∀𝑥 .𝜚 𝑐 (𝑥) =⇒ 𝜎 (𝑥)), i.e. |= 𝜚 𝑐 (𝑑𝑐 ) ∧ ¬𝜎 (𝑑𝑐 )for some 𝑑𝑐 .
The validity of 𝜚 𝑐 (𝑑𝑐 ) can be reduced to the termination problem, as in the previous section,
because 𝜚 𝑐 is the minimum solution. The corresponding constraint set is∀𝑧.

𝐷𝑐 (𝑧) ∧ ¬𝜗𝑐 (𝑧) =⇒ 𝐷𝑐 (𝑓𝑐,1 (𝑧)) ∧ 𝐷𝑐 (𝑓𝑐,2 (𝑧))∧ 𝑊𝑐 (𝑧, 𝑓𝑐,1 (𝑧)) ∧ 𝑊𝑐 (𝑧, 𝑓𝑐,2 (𝑧)) ∧ 𝜏 (𝑓𝑐,1 (𝑧), 𝑓𝑐,2 (𝑧), 𝑧)

WF (𝑊𝑐 )𝐷𝑐 (𝑑𝑐 )(3)

where 𝜗𝑐 (𝑥) = (𝜗 (𝑥) ∨𝑥 = 𝑐) and all predicate variables have subscript 𝑐 expressing the dependency.
The main difference with (2) is that the candidate minimal solution 𝜗 is replaced with the predicate
variable 𝐷𝑐 representing (an underapproximation of) the minimum solution.
Proposition 5.5. The CHC system (1) has no solution containing 𝜗𝑐 if and only if(3) ∪ {¬𝜎 (𝑑𝑐 )}is satisfiable. Here 𝑑𝑐 appearing in (3) and in ¬𝜎 (𝑑𝑐 ) is regarded as a nullary function symbol, thevalue of which should be specified by a solution.
□

Proof. Similar to the proof of Theorem 5.3.

The solution 𝜗 is maximal if and only if the condition in the above proposition is true for every 𝑐with |= ¬𝜗 (𝑐). Collecting solutions for all 𝑐, we define𝑔(𝑐) := 𝑑𝑐

𝑓1 (𝑐, 𝑥) := 𝑓𝑐,1 (𝑥)′𝑓2 (𝑐, 𝑥) := 𝑓𝑐,2 (𝑥)′𝑊 ((𝑐, 𝑥), (𝑐 , 𝑦)) :⇔ (𝑐 = 𝑐 ) ∧ 𝑊𝑐 (𝑥, 𝑦)𝐷 (𝑐, 𝑥) :⇔ 𝐷𝑐 (𝑥)Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:17

where 𝑑𝑐 , 𝑓𝑐,1, 𝑓𝑐,2,𝑊𝑐 and 𝐷𝑐 are solutions of the constraint set in Proposition 5.5 if |= ¬𝜗 (𝑐);otherwise 𝐷𝑐 = 𝑊𝑐 = ⊥ and 𝑑𝑐 , 𝑓𝑐,1 and 𝑓𝑐,2 are arbitrary. The constraints for these functions andrelations are given by:∀𝑥 .

¬𝜗 (𝑥) =⇒ 𝐷 (𝑥, 𝑔(𝑥)) ∧ ¬𝜎 (𝑔(𝑥))∀𝑥, 𝑧.

𝐷 (𝑥, 𝑧) ∧ ¬(𝜗 (𝑧) ∨ 𝑧 = 𝑥) ∧ ¬𝜗 (𝑥)=⇒ 𝐷 (𝑥, 𝑓1 (𝑥, 𝑧)) ∧ 𝐷 (𝑥, 𝑓2 (𝑥, 𝑧)) ∧ 𝑊 ((𝑥, 𝑧), (𝑥, 𝑓1 (𝑥, 𝑧)))∧ 𝑊 ((𝑥, 𝑧), (𝑥, 𝑓2 (𝑥, 𝑧))) ∧ 𝜏 (𝑓1 (𝑥, 𝑧), 𝑓2 (𝑥, 𝑧), 𝑧)
WF (𝑊 ).

(4)

Theorem 5.6. 𝜗 is a maximal solution of (1) if and only if the constraint set (4) is satisfiable.

□

Example 5.7. Consider the following system of CHCs:
𝑃 (1),∀𝑥, 𝑦. 𝑃 (𝑥) ∧ 𝑃 (𝑦) =⇒ 𝑃 (𝑥 + 𝑦),∀𝑥 . 𝑃 (𝑥) =⇒ 𝑥 ≥ −5.

Then the unique maximal solution is 𝜗 (𝑥) = (𝑥 ≥ 0). The constraint set expressing the termination
problem is:∀𝑥 . 𝑥 < 0 =⇒ 𝐷 (𝑥, 𝑔(𝑥)) ∧ 𝑔(𝑥) < −5∀𝑥, 𝑧.

𝐷 (𝑥, 𝑧) ∧ ¬(𝑧 ≥ 0 ∨ 𝑧 = 𝑥) ∧ ¬(𝑥 ≥ 0)=⇒ 𝐷 (𝑥, 𝑓1 (𝑥, 𝑧)) ∧ 𝐷 (𝑥, 𝑓2 (𝑥, 𝑧)) ∧ 𝑊 ((𝑥, 𝑧), (𝑥, 𝑓1 (𝑥, 𝑧)))∧ 𝑓1 (𝑥, 𝑧) + 𝑓2 (𝑥, 𝑧) = 𝑧 ∧ 𝑊 ((𝑥, 𝑧), (𝑥, 𝑓2 (𝑥, 𝑧)))WF (𝑊 ).
A solution is 𝐷 (𝑥, 𝑦) = (𝑥 < 0 ∧ (∃𝑛.(1 ≤ 𝑛 ≤ 6) ∧ (𝑦 = 𝑛𝑥)), 𝑊 ((𝑥, 𝑦), (𝑥, 𝑦 ′)) = (𝑦 < 𝑦 ′ < 0),𝑔(𝑥) = 6𝑥, 𝑓1 (𝑥, 𝑦) = 𝑥, and 𝑓2 (𝑥, 𝑦) = (𝑦 − 𝑥).
□
6

CHC OPTIMIZATION METHODThis section describes our CHC optimization procedure using the reductions of (non)optimality
checking to constraint satisfaction problems given in Section 5. We first explain the overall flowof our procedure (Section 6.1) and define a class of satisfaction problems, pfwnCSP, to which
the (non)maximality checking problem is reduced (Section 6.2). We then give reductions of(non)maximality checking to pfwnCSP (Section 6.3) and develop a data-driven solver for pfwnCSP(Section 6.4).
6.1

CHC Optimization via Iterated Satisfaction

Given a CHC optimization problem maximize {𝑃1, . . . , 𝑃𝑚 } s.t. C, our procedure starts from anarbitrary solution 𝜃 of C and iteratively updates 𝜃 until it becomes optimal. In each step, ourprocedure checks if there exists a solution 𝜃 ′ of C such that
𝜃 (𝑃1 ) ⊊ 𝜃 ′ (𝑃 1 ) ∧ 𝜃 (𝑃2 ) ⊆ 𝜃 ′ (𝑃 2 ) ∧ . . . ∧ 𝜃 (𝑃𝑛 ) ⊆ 𝜃 ′ (𝑃𝑛 ).

(5)

That means, 𝜃 ′ is not worse than 𝜃 for 𝑃2, . . . , 𝑃𝑛 and 𝜃 ′ strictly improves 𝜃 on 𝑃1 . Note that theexistence (resp. absence) of such a solution 𝜃 ′ is reducible to a constraint satisfaction problem as
discussed in Section 5.1 (resp. Section 5.3). If such a solution 𝜃 ′ is found, set 𝜃 to 𝜃 ′ and continue
the procedure. If the absence of such a solution is confirmed, it suffices to solve the subproblem
maximize {𝑃2, . . . , 𝑃𝑚 } s.t. C ∪ {∀®
𝑥 1 .𝜑 1 (𝑥®1 ) ⇒ 𝑃 1 (𝑥®1 ), . . . , ∀®
𝑥𝑛 .𝜑𝑛 (𝑥®𝑛 ) ⇒ 𝑃𝑛 (𝑥®𝑛 )}Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:18

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

Algorithm 1: Optimize
Input: A CHC Optimization Problem (mode, Δ, C, [𝑃 1 ; . . . ; 𝑃𝑚 ])Output: OptSat(𝜃 ) if an optimal solution 𝜃 is found, Unsat if C is not satisfiable
1 procedure Optimize (mode, Δ, C, [𝑃 1 ; . . . ; 𝑃𝑚 ]) =2
case Solve(C) of
3| Sat(𝜃 ) → Aux(mode, Δ, C, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃, ∅);4| Unsat → return Unsat;
5 end
6 procedure Aux (mode, Δ, C, [𝑃 1 ; . . . ; 𝑃𝑚 ], 𝜃, 𝜃 0 ) =7
if 𝑚 = 0 then return OptSat(𝜃 ⊎ 𝜃 0 );8
result := parallel any
9■ Solve(IsOpt(mode, Δ, C, 𝑃1, [𝑃2 ; . . . ; 𝑃𝑚 ], 𝜃 )) ;10
■ Solve(IsNonOpt(mode, Δ, C, 𝑃1, [𝑃2 ; . . . ; 𝑃𝑚 ], 𝜃 )) ;11
case result of12| First(Sat(_)) | Second(Unsat) →13
Δ ′ := Δ \ {𝑃1 };14
C ′ := 𝜃 ↾𝑃1 (CΔ );15
𝜃 0′ := 𝜃 0 ∪ {𝑃1 ↦→ 𝜃 (𝑃 1 )};16
Aux(mode, Δ ′, C ′, [𝑃 2 ; . . . ; 𝑃𝑚 ], 𝜃, 𝜃 0′ )17
| Second(Sat(𝜃 refined )) →18
Aux(mode, Δ, C, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 refined , 𝜃 0 )19| First(Unsat) →20
Sat(𝜃 refined ) := Solve(IsNonOpt(mode, Δ, C, 𝑃1, [𝑃 2 ; . . . ; 𝑃𝑚 ], 𝜃 ));21
Aux(mode, Δ, C, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 refined , 𝜃 0 )22 endwhere 𝜑𝑖 = 𝜃 (𝑃𝑖 ) for each 𝑖. In this subproblem, the predicate variable 𝑃 1 is no longer a target of
optimization as it has already been optimized. Furthermore the subpreblem requires that a solution
subsumes the current solution 𝜃 . A minimization problem minimize {𝑃1, . . . , 𝑃𝑚 } s.t. C can besolved similarly.
Algorithm 1 formally describes our procedure Optimize for solving a given CHC optimization
problem. Optimize(↑, Δ, C, [𝑃1 ; . . . ; 𝑃𝑚 ]) computes a solution of maximize {𝑃 1, . . . , 𝑃𝑚 } s.t. C,
where Δ is the sort assignment for predicate variables in CHCs C, and Optimize(↓, Δ, C, [𝑃1 ; . . . ; 𝑃𝑛 ])computes a solution of minimize {𝑃1, . . . , 𝑃𝑚 } s.t. C. Optimize first computes any solution of C
and then iteratively updates the solution until it becomes optimal, using the auxiliary procedure
Aux.
Aux(mode, Δ, C, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃, 𝜃 0 ) returns an optimal solution 𝜃 opt that is better than 𝜃 (i.e.,
if mode = ↑, we have 𝜃 (𝑃𝑖 ) ⊆ 𝜃 opt (𝑃𝑖 ), and otherwise 𝜃 (𝑃𝑖 ) ⊇ 𝜃 opt (𝑃𝑖 )). The basic idea of
Aux has already explained at the beginning of this subsection. It reduces the existence andabsence of a better solution (i.e. a solution satisfying (5)) to constraint satisfaction problems,
IsNonOpt(mode, Δ, C, 𝑃1, [𝑃 2 ; . . . ; 𝑃𝑚 ], 𝜃 ) and IsOpt(mode, Δ, C, 𝑃1, [𝑃 2 ; . . . ; 𝑃𝑚 ], 𝜃 ), respectively,
and solves these problems by using a solver Solve. The two constraint satisfaction problems are

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:19

solved in parallel.11 At the case analysis on Line 11, the first case is when the absence of a better
solution is confirmed, and the second and third cases are when its existence is ensured. In the thirdcase, the return value Unsat for Solve(IsOpt(mode, Δ, C, 𝑃1, [𝑃 2 ; . . . ; 𝑃𝑚 ], 𝜃 ) only tells us existenceof a better solution without providing any witness, so we need to compute a better solution bysolving IsNonOpt(mode, Δ, C, 𝑃1, [𝑃2 ; . . . ; 𝑃𝑚 ], 𝜃 ).
We explain the sub-procedures IsOpt, IsNonOpt, and Solve in more details in Sections 6.3 and 6.4.
Note that the classes of constraints generated by IsOpt and IsNonOpt go beyond CHCs: IsNonOpt
requires CHCs extended with non-emptiness constraints and IsOpt requires pfwCSP [Unno et al.
2021], which extends CHCs with non-Horn clauses, well-foundedness, and functionality constraints.
We thus introduce the class pfwnCSP that incorporates all the required extensions first in the next
section.
6.2

pfwnCSP: Extending CHCs

We introduce an extension of CHCs that are equivalent to those in Unno et al. [2021].12
A constrained clause is a formula of the form
!
!
𝑙
𝑚
Ü
Ü
∀®
𝑦. 𝜙 ∨𝑃𝑖 (𝑥®𝑖 ) ∨¬𝑃𝑖 (𝑥®𝑖 ) ,
𝑖=1

𝑖=𝑙+1

or equivalently,∀®
𝑦.

𝑃ℓ+1 (𝑥 ℓ+1® ) ∧ · · · ∧ 𝑃𝑚 (𝑥®𝑚 ) ∧ 𝜑 ⇒ (𝑃1 (𝑥®1 ) ∨ · · · ∨ 𝑃ℓ (𝑥®ℓ )),where 𝜑 is a formula in the constraint language, 𝑃1, . . . , 𝑃𝑚 are predicate variables and 0 ≤ ℓ ≤ 𝑚.
A predicate Constraint Satisfaction Problem (pCSP) C is the problem to find a solution of a finite setof clauses [Satake et al. 2020]. Here, as usual, a solution is an interpretation of predicate variables
that satisfies all given clauses. The notion of constrained clause is a generalization of constrainedHorn clause: a constrained Horn clause is a constrained clause with ℓ = 0, 1. Hence pCSP is a
generalization of the CHC Satisfaction Problem.
We introduce the new class pfwnCSP that further extends pCSP by allowing following constraints:• Non-emptiness constraint: 𝑃 ≠ ∅ where 𝑃 is a predicate variable. This constraint requires thatthe interpretation of 𝑃 in a solution 𝜃 must be non-empty, i.e. 𝜃 (𝑃) ≠ ∅.
• Well-foundedness constraint: WF (𝑃) where 𝑃 is a binary relation on a certain sort. This
constraint requires that the interpretation of 𝑃 in a solution 𝜃 is well-founded, i.e. there is no
infinite sequence 𝑎 1, 𝑎 2, . . . such that 𝜃 (𝑃) (𝑎𝑖 , 𝑎𝑖+1 ) holds for every 𝑖.
A constraint may have function variables in addition to predicate variables. A pfwnCSP C is a finite
set of constraints over predicate variables and function variables, consisting of constrained clauses,
non-emptiness constraints, and well-foundedness constraints.
The formal definition of pfwnCSP used in this paper is as follows. Assume a signature Σ and astructure A, fixed in the sequel.
The set of sorts is defined by the following grammar:𝑆::=

𝛼 | 𝑆 1 × 𝑆 2 | 𝑆 1 + 𝑆 2,

11 In Algorithm 1, the parallel any statement (Line 8) runs the given two statements in parallel and stops when one is over.

If the first statement (resp. the second statement) terminates and returns a value 𝑣, then the value of parallel any is First(𝑣)(resp. Second(𝑣)).
12 An additional feature is non-emptiness constraint. Although this constraint is definable using a function variable (since𝑃 ≠ ∅ is equivalent to 𝑃 (𝑓 ()) for a fresh nullary function variable 𝑓 ), non-emptiness constraint is preferable since it iseasier than general function variables.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:20Yu Gu, Takeshi Tsukada, and Hiroshi Unno

where 𝛼 ranges over basic sorts specified by the signature Σ, 𝑆 1 × 𝑆 2 is the product sort and 𝑆 1 + 𝑆 2 isthe sum sort, of which the interpretation is the disjoint union AJ𝑆 1 K + AJ𝑆 2 K of the interpretationsof 𝑆 1 and 𝑆 2 . A term of sort 𝜎 is defined as usual. In particular, if 𝑡 1 and 𝑡 2 are terms of sort 𝑆 1 and𝑆 2 , then (𝑡 1, 𝑡 2 ) is a term of sort 𝑆 1 × 𝑆 2 and inj𝑖 (𝑡𝑖 ) (𝑖 = 1, 2) is a term of sort 𝑆 1 + 𝑆 2 .
Remark 4. An important difference from the setting in Section 3 is the sum sort 𝑆 1 + 𝑆 2 . The sum
sort is useful to pack multiple predicates into a single predicate: if 𝑃𝑖 is a predicate over 𝑆𝑖 for
𝑖 = 1, . . . , 𝑛, the tuple (𝑃1, . . . , 𝑃𝑛 ) of 𝑛 predicates can be represented by a single predicate 𝑄 overthe sort 𝑆 1 + · · · + 𝑆𝑛 defined by 𝑄 (inj𝑖 (𝑥)) :⇔ 𝑃𝑖 (𝑥).
□A sort environment Δ is a finite set of sort declarations of the forms 𝑃 : 𝑆 → Prop and 𝑓 : 𝑆 → 𝑆 ′.
Given Δ, the set of formulas possibly using predicate variables and function variables in Δ is definedas usual. We shall consider only well-sorted formulas.
Definition 6.1. A pfwnCSP (Δ, C) is a pair of a sort environment and a finite set of constraints
over predicate variables and function variables, consisting of constrained clauses, non-emptinessconstraints, and well-foundedness constraints. We assume that 𝑓 : 𝑆 → 𝑆 ′ ∈ Δ implies that 𝑆 ′ does
not contain the sort constructor +. The set of constraints must satisfy the following conditions:• For each predicate variable 𝑃, the set C contains at most one of 𝑃 ≠ ∅ and WF (𝑃).
• If WF (𝑃) ∈ C, then (𝑃 : 𝑆 × 𝑆 → Prop) ∈ Δ for some 𝑆.
A solution 𝜃 of C is an assignment to a predicate variable (𝑃 : 𝑆 → Prop) ∈ Δ a predicate 𝜃 (𝑃) ⊆AJ𝑆K and to a function variable (𝑓 : 𝑆 → 𝑆 ′) ∈ Δ a function 𝜃 (𝑓 ) : AJ𝑆K → AJ𝑆 ′K that satisfies
all constraints in C. The semantics of additional constraints are given as follows.
• 𝜃 |= 𝑃 ≠ ∅ if 𝜃 (𝑃) ≠ ∅.
• 𝜃 |= WF (𝑃) (where (𝑃 : 𝜎 × 𝜎 → Prop) ∈ Δ) if there is no infinite sequence 𝑎 1, 𝑎 2, . . . ofelements in AJ𝜎K such that 𝜃 (𝑃) (𝑎𝑖 , 𝑎𝑖+1 ) holds for every 𝑖.
□
6.3

Constraint Generation

This subsection describes the subprocedures IsOpt and IsNonOpt, which reduce the absence andexistence of a better solution to pfwnCSP. The basic idea has already explained in Section 5.
The sub-procedure IsNonOpt(↑, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ) is rather straightforward. We would
like to have a constraint set characterizing the subset of solutions 𝜃 ′ of C such that 𝜃 (𝑃𝑖 ) ⊆ 𝜃 ′ (𝑃𝑖 )for 𝑖 = 1, . . . , 𝑚 and 𝜃 (𝑃) ⊊ 𝜃 ′ (𝑃). We define13
IsNonOpt(↑, Δ, C, 𝑃, [𝑃 1 ; . . . ; 𝑃𝑚 ], 𝜃 )no:= C ∪ ∀𝑥®𝑖 . 𝜃 (𝑃𝑖 ) (𝑥®𝑖 ) ⇒ 𝑃 (𝑥®𝑖 ) | 1 ≤ 𝑖 ≤ 𝑚n∪∀®
𝑥 . 𝜃 (𝑃) (𝑥)® ∨ 𝑁 (𝑥)® ⇒ 𝑃 (𝑥),®
∀®
𝑥 . 𝜃 (𝑃) (𝑥)® ∧ 𝑁 (𝑥)® ⇒ ⊥,𝑁 ≠ ∅ }.

Here the predicate sort environment Δ ′ for the generated constraint set is Δ ⊎ {𝑁 : 𝑆 → Prop},
where 𝑁 is a fresh predicate variable and 𝑆 → Prop is the sort of 𝑃. The first and second parts saythat a solution of IsNonOpt(↑, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ) is not worse than 𝜃 on {𝑃 1, . . . , 𝑃𝑚 }, and thethird part says that a solution is strictly better than 𝜃 on 𝑃. The predicate 𝑁 under-approximates thedifference 𝜃 ′ (𝑃) \ 𝜃 (𝑃) between the current solution 𝜃 and a solution 𝜃 ′ of the generated constraint
set. The inclusion between 𝜃 ′ (𝑃) and 𝜃 (𝑃) must be strict since 𝑁 must be non-empty. The definition
13 Although ∀®
𝑥 .𝜃 (𝑃 ) (𝑥)® ∨ 𝑁 (𝑥)® ⇒ 𝑃 (𝑥)® is not a clause, it is equivalent to the conjunction of clauses ∀®
𝑥 .𝜃 (𝑃 ) (𝑥)® ⇒ 𝑃 (𝑥)®

and ∀®
𝑥 .𝑁 (𝑥)® ⇒ 𝑃 (𝑥).
® We shall implicitly use this kind of equivalences in this subsection to simplify the presentation.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:21

of IsNonOpt(↓, Δ, C, 𝑃, [𝑃 1 ; . . . ; 𝑃𝑚 ], 𝜃 ) is similar:
IsNonOpt(↓, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 )no:= C ∪ ∀𝑥®𝑖 . 𝑃 (𝑥®𝑖 ) ⇒ 𝜃 (𝑃𝑖 ) (𝑥®𝑖 ) | 1 ≤ 𝑖 ≤ 𝑚n∪∀®
𝑥 . 𝑃 (𝑥)® ∨ 𝑁 (𝑥)® ⇒ 𝜃 (𝑃) (𝑥),®
∀®
𝑥 . 𝑃 (𝑥)® ∧ 𝑁 (𝑥)® ⇒ ⊥,𝑁 ≠ ∅ }.

Note that IsNonOpt(mode, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ) belongs to the class of CHCs extended with
non-emptiness constraints.
The correctness of the generated constraint sets is straightforward.
Lemma 6.2. Let 𝜃 be a solution of (Δ, C).
• For every solution 𝜃 ′ of IsNonOpt(mode, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ), we have 𝜃 (𝑃𝑖 ) ≤mode 𝜃 ′ (𝑃𝑖 )for 𝑖 = 1, . . . , 𝑚 and 𝜃 (𝑃) <mode 𝜃 ′ (𝑃).
• If there exists a solution 𝜃 ′ of C such that 𝜃 (𝑃𝑖 ) ≤mode 𝜃 ′ (𝑃𝑖 ) for 𝑖 = 1, . . . , 𝑚 and 𝜃 (𝑃) <mode𝜃 ′ (𝑃), then IsNonOpt(mode, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ) is satisfiable.
□
The subprocedure IsOpt(mode, Δ, C, 𝑃, [𝑃1 ; . . . ; 𝑃𝑚 ], 𝜃 ) is more complicated. Let us first explain
the main differences from the setting in Sections 5.2 and 5.3.
• The number of predicate variables in C may be greater than 1.
• Only a part of the predicate variables is the target of optimization.
• For each predicate variable 𝑄, C may have more than 1 clauses of the form · · · ⇒ 𝑄 (𝑥).
®
These differences are not essential and the ideas discussed in Sections 5.2 and 5.3 are applicableto general CHCs. Roughly speaking, these gaps can be filled by preprocessing of CHCs. Afterthe preprocessing, the CHCs has a single “large” predicate obtained by combining all predicate
variables in Δ. When Δ = {𝑃𝑖 : 𝑆𝑖 → Prop | 1 ≤ 𝑖 ≤ 𝑛}, such Ía “large” predicate variable 𝑅
has sort (𝑆 1 + 𝑆 2 + · · · + 𝑆𝑛 ) → Prop, which is abbreviated as ( 𝑛𝑖=1 𝑆𝑖 ) → Prop, and satisfies∀𝑥 : 𝑆𝑖 .𝑅(inj𝑖 (𝑥)) ⇔ 𝑃𝑖 (𝑥). The constraint generation for the optimality checking given below isbasically obtained by this way.
We introduce some notations and conventions. For each 𝑄 ∈ dom(Δ), we write 𝑆𝑄 for the sort of
the argument of 𝑄 (i.e. 𝑄 : 𝑆𝑄 → Prop ∈ Δ). For simplicity, we assume that the constraint language
admits the quantifier elimination (or equivalently, the existential quantifier can be used freely inthe constraint language). Then, under a mild assumption on the constraint language, each CHC
can be written as∀𝑦1 : 𝑆𝐿1 . . . . ∀𝑦𝑛 : 𝑆𝐿𝑛 .∀𝑧 : 𝑆𝑄 .𝜑 (𝑦1, . . . , 𝑦𝑛 , 𝑧) ∧ 𝐿1 (𝑦1 ) ∧ · · · ∧ 𝐿𝑛 (𝑦𝑛 ) ⇒ 𝑄 (𝑧)or its variant with ⊥ at the head position. We assume that each CHC is of the above form. When R
is the above CHC, 𝑆 Head ( R) = 𝑆𝑄 and 𝑆 Body ( R) = 𝑆𝐿1 × · · · × 𝑆𝐿𝑛 . The subset Ð
C [𝑄] (resp. C [⊥]) of C
consists of those with 𝑄 (rsep. ⊥) at the head position. Then C = C [⊥] ∪ 𝑄 ∈dom(Δ) C [𝑄].
Figure 3 shows the constraint set for checking the minimality of a given solution. In every solution,
the interpretation of 𝐷𝑄 is an under-approximation of the interpretation of 𝑄 in the minimum
solution of C. Hence the constraint ∀𝑥 : 𝑆𝑃 .𝜃 (𝑃) (𝑥) ⇒ 𝐷 𝑃 (𝑥) ensures that 𝜃 coincides with theminimum solution of C on 𝑃. The predicate variable𝑊 and function variables 𝑓 R are used to describe
the minimality requirements for (𝐷𝑄 )𝑄 ∈dom(Δ) andÍcorrespond to 𝑊Íand 𝑓 (𝑧) = (𝑓1 (𝑧), 𝑓2 (𝑧))in the constraint set (2) in Section 5.2. The sort ( 𝑄 ∈dom(Δ) 𝑠𝑄 ) × ( 𝑄 ∈dom(Δ) 𝑠𝑄 ) → Prop of
𝑊 can be explained by the intuition Íthat we are reasoning about a CHC system with a single“large” predicate variable 𝑅 of sort ( 𝑄 ∈dom(Δ) 𝑠𝑄 ) → Prop. The constraint ∀𝑥 : 𝑆𝑄 . 𝐷𝑄 (𝑥) ⇒ÔR ∈ C [𝑄 ] ProvableBy R (𝑥) requires that, if 𝐷𝑄 (𝑥) is true, this fact should be justified by a clauseÓ
R in C [𝑄]. A clause R ≡ ∀𝑥𝑦.𝜑® (𝑥, 𝑦)® ∧ 𝑘𝑖=1 𝐿𝑖 (𝑦𝑖 ) ⇒ 𝑄 (𝑥) justifies 𝐷𝑄 (𝑎) if there exist 𝑏®
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:22

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

Δ′ ≜{𝐷𝑄 : 𝑆𝑄 → Prop | 𝑄 ∈ dom(Δ)}ÍÍ
𝑄 ∈dom(Δ) 𝑠𝑄 ) × ( 𝑄 ∈dom(Δ) 𝑠𝑄 ) → Prop}⊎{𝑊 : (⊎{𝑓 R : 𝑆 Head ( R) → 𝑆 Body ( R) | R ∈ C [𝑄] for some 𝑄 ∈ dom(Δ)}

C′ ≜∪{WF (𝑊 ),∀𝑥 : 𝜎𝑃 . 𝜃 (𝑃) (𝑥) ⇒ 𝐷 𝑃 (𝑥)}ÔR ∈ C [𝑄 ] ProvableBy R (𝑧) | 𝑄 ∈ dom(Δ)}{∀𝑧 : 𝑠𝑄 . 𝐷𝑄 (𝑧) ⇒ProvableBy R (𝑧) ≜𝜑 (𝑓 R (𝑧), 𝑧) ∧

𝑛
Û



𝐷 𝐿𝑖 𝜋𝑖 (𝑓 R (𝑧) ∧ 𝑊 inj𝑄 (𝑧), inj𝐿𝑖 (𝜋𝑖 (𝑓 R (𝑧)))𝑖=1hif R is ∀𝑦1 . . . 𝑦𝑛 𝑧.𝜑 ((𝑦1, . . . , 𝑦𝑛 ), 𝑧) ∧ 𝐿1 (𝑦1 ) ∧ · · · ∧ 𝐿𝑛 (𝑦𝑛 ) ⇒ 𝑄 (𝑧)iFig. 3. pfwCSP Constraint Generation IsOpt (↓, Δ, C, 𝑃, X, 𝜃 ) ≜ (Δ ′, C ′ ) for CHC Minimality Checking® holds and 𝐷 𝐿 (𝑏𝑖 ) has a “smaller witness” than 𝐷𝑄 (𝑎). The auxiliary predicate
such that 𝜑 (𝑎, 𝑏)𝑖ProvableBy R (𝑥) describes this property, assuming that 𝑏® is given by 𝑓 R (𝑥).
The constraint set IsOpt (↑, CΔ, 𝑃, X, 𝜃 ) for the maximality checking is given in Figure 4. Following
the discussion in Section 5.3, we would like to give a constraint set describing the following
condition:
ÐFor each 𝑎 such that ¬𝜃 (𝑃) (𝑎), let 𝜃 𝑎′ be the least solution of 𝑄 ∈dom(Δ) C [𝑄] that′
additionally satisfies 𝜃 (𝑃) (𝑥) ∨ (𝑥 = 𝑎) ⇒ 𝜃 𝑎 (𝑃) and 𝜃 (𝑄) (𝑥) ⇒ 𝜃 𝑎′ (𝑄) (𝑥) (for each𝑄 ∈ X). Then 𝜃 𝑎′ violates some rule in C [⊥].
Constraints for under-approximations of 𝜃 𝑎′ are given by the same idea as the minimality checking.
The predicate variables 𝐷𝑄 and 𝑊 and function variables 𝑓 R are essentially the same as those in theminimal case, except that those variables for the maximality checking have additional parameters ofsort 𝑆𝑃 corresponding to 𝑎. The assignment 𝜃ˆ(𝑄) (𝑎, −) is the lower bound for 𝜃 𝑎′ (𝑄). The constraintÔ∀𝑥 : 𝑆𝑃 . ¬𝜃 (𝑃) (𝑥) ⇒ R ∈Δ [⊥] FailAt R (𝑥) requires the violation of 𝜃 𝑥′ to some R ∈ C [⊥].
The correctness of IsOpt (mode, Δ, C, 𝑃, X, 𝜃 ) can be proved by arguments similar to those in
Sections 5.2 and 5.3. The generated constraints belong to the subclass pfwCSP [Unno et al. 2021] of
pfwnCSP without non-empty predicates.
6.4 Data-Driven pfwnCSP Solving
The sub-procedure Solve is for solving a pfwnCSP (Δ, C). Our procedure Solve is an extension ofan existing data-driven method for solving pfwCSP over LIA [Unno et al. 2021] with non-emptinessconstraints. Solve is based on CounterExample Guided Inductive Synthesis (CEGIS).
Before entering the CEGIS process, Solve eliminates non-emptiness constraints. It transform(𝑃 ≠ ∅) ∈ C into a pair of a singleton set constraint, singleton(𝑄), and a clause ∀𝑥 .𝑄 (𝑥) ⇒ 𝑃 (𝑥),where 𝑄 is a fresh predicate variable. The singleton set constraint singleton(𝑄) requires that asolution assigns a singleton set to 𝑄, as expected.
Solve iteratively accumulates example instances E of the original constraints (Δ, C), which
are instances of clauses obtained by substituting variables with concrete values. For example, if∀𝑥𝑦𝑧.𝜑 (𝑥, 𝑦, 𝑧) ∧ 𝑃 (𝑥) ∧ 𝑄 (𝑦) ⇒ 𝑇 (𝑧) belongs to C, then 𝜑 (1, 2, 3) ∧ 𝑃 (1) ∧ 𝑄 (2) ⇒ 𝑇 (3) and𝜑 (−8, 23, 9) ∧ 𝑃 (−8) ∧ 𝑄 (23) ⇒ 𝑇 (0) are example instances. We are interested only in example
instances whose constraints (i.e. 𝜑 (1, 2, 3) and 𝜑 (−8, 23, 9) in the previous examples) are true,and call 𝑃 (1) ∧ 𝑄 (2) ⇒ 𝑇 (3) and 𝑃 (−8) ∧ 𝑄 (23) ⇒ 𝑇 (0) examples instances as well (provided
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

Δ′ ≜

21:23

{𝐷𝑄 : 𝑆𝑃 × 𝑆𝑄 → Prop | 𝑄 ∈ dom(Δ)}ÍÍ
𝑄 ∈dom(Δ) 𝑆𝑄 )) × (𝑆 𝑃 × ( 𝑄 ∈dom(Δ) 𝑆𝑄 )) → Prop}⊎{𝑊 : (𝑆𝑃 × (⊎{𝑓 R : 𝑆𝑃 × 𝑆 Head ( R) → 𝑆 Body ( R) | R ∈ C [𝑄] for some 𝑄 ∈ dom(Δ)}⊎{𝑔 R : 𝑆𝑃 → 𝑆 Body ( R) | R ∈ C [⊥]}C′ ≜∪{WF (𝑊 ),∀𝑥 : 𝑆𝑃 . ¬𝜃 (𝑃) (𝑥) ⇒ÔR ∈Δ [⊥] FailAt R (𝑥)}Ô{∀𝑥 : 𝑆𝑃 .∀𝑧 : 𝑆𝑄 . ¬𝜃 (𝑃) (𝑥) ∧ 𝐷𝑄 (𝑥, 𝑧) ⇒ 𝜃ˆ(𝑄) (𝑥, 𝑧) ∨ R ∈ C [𝑄 ] ProvableBy R (𝑥, 𝑧)| 𝑄 ∈ dom(Δ)}

ProvableBy R (𝑥, 𝑧) ≜𝜑 (𝑧, 𝑓 R (𝑥, 𝑧))𝑛Û𝐷 𝐿𝑖 𝜋𝑖 (𝑓 R (𝑥, 𝑧) ∧ 𝑊 (𝑥, inj𝑄 (𝑧)), (𝑥, inj𝐿𝑖 (𝜋𝑖 (𝑓 R (𝑥, 𝑧))))
∧
𝑖=1

h

if R is ∀𝑥𝑦1 . . . 𝑦𝑛 .𝜑 (𝑥, (𝑦1, . . . , 𝑦𝑛 )) ∧ 𝐿1 (𝑦1 ) ∧ · · · ∧ 𝐿𝑛 (𝑦𝑛 ) ⇒ 𝑄 (𝑥)FailAt R (𝑥) ≜𝜑 (𝑔 R (𝑥)) ∧𝑛Û𝐷 𝐿𝑖 𝑥, 𝜋𝑖 (𝑔 R (𝑥)

i



𝑖=1

h

if R is ∀𝑦1 . . . 𝑦𝑛 .𝜑 (𝑦1, . . . , 𝑦𝑛 ) ∧ 𝐿1 (𝑦1 ) ∧ · · · ∧ 𝐿𝑛 (𝑦𝑛 ) ⇒ ⊥𝜃ˆ(𝑄) (𝑥, 𝑧) ≜
𝜃 (𝑃) (𝑧) ∨ (𝑥 = 𝑧)𝜃 (𝑄) (𝑧)


⊥


i

if 𝑄 = 𝑃
if 𝑄 ∈ X
otherwise

Fig. 4. pfwCSP Constraint Generation IsOpt (↑, Δ, C, 𝑃, X, 𝜃 ) ≜ (Δ ′, C ′ ) for CHC Maximality Checking

that 𝜑 (1, 2, 3) and 𝜑 (−8, 23, 9) are true). Note that all example instances come from clauses; nonemptiness constraints and well-foundedness constraints do not generate example instances.
The main iteration of CEGIS consists of the following two phases:• Synthesis Phase: find a candidate solution 𝜃 that satisfies all the examples in E;• Validation Phase: check whether the candidate 𝜃 also satisfies the original constraints(Δ, C), and if so, return 𝜃 as a genuine solution, and otherwise repeat the procedure with E
extended with counterexamples.
The synthesis phase of our procedure Solve is template-based. A template of a predicate ofarity 𝑛 is a formula 𝜓 (𝑥 1, . . . , 𝑥𝑛 ; 𝑐 1, . . . , 𝑐𝑚 ) with extra variables 𝑐 1, . . . , 𝑐𝑚 . The extra variables are
regarded as constants that have not yet been determined, and fixing their values determines a
predicate. Similarly a template of a function is an expression with extra variables. In the synthesis
phase, the solver prepares a template for each predicate variable and function variable. Substituting
each predicate/function variable in E to the template results in a set of constraints over extra
variables. The solver chooses templates carefully so that constraints after substitution can be solved
by an SMT solver, and hence appropriate values of extra variables can be computed by an SMT
solver.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:24

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

The templates are chosen so that non-emptiness constraints and well-foundedness constraints
are satisfied independent of the values of extra variables. If WF (𝑃) ∈ C, then a template for 𝑃 (𝑥, 𝑦)
is 𝑓 (𝑥) ≥ 0 ∧ 𝑓 (𝑦) ≥ 0 ∧ 𝑓 (𝑥) > 𝑓 (𝑦) for a fresh function variable 𝑓 .14 It is easy to see that thispredicate is well-founded for every function 𝑓 . A template for 𝑄 with the singleton set constraint
singleton(𝑄) is 𝑥 = 𝑒, where 𝑒 is an expression with extra variables.
The choice of template significantly affects the performance of the solver. The strategy ofthe solver by Unno et al. [2021] is based on stratified families of templates, which are designed
for enumerating candidate predicates in a prioritized manner: starting from a less expressive
initial template for each predicate variable, the solver gradually refines it in a counterexampleguided manner if no solution exists in the current template. The stratification of templates andthe counterexample-guided refinement thus automatically adjust the expressiveness of templates
depending on the complexity of solutions for the target constraint set. See Unno et al. [2021] fordetails.
The validation phase is straightforward since what we need to check is only the validity ofclauses. We just to need to invoke an SMT solver.
7

IMPLEMENTATION AND EVALUATION

Section 4 has shown that the CHC optimization problem is Π 02 -complete (Theorem 4.2). A natural
question to ask is whether there is any possibility to realize a practical CHC optimization tool
despite the theoretical hardness. The goal of this section is to provide an initial positive answer via
preliminary experiments.
To this end, we implemented a prototype CHC optimization tool called OptPCSat based on
Algorithm 1 using the Multicore OCaml language for concurrent programming. We extended
an existing tool PCSat [Unno et al. 2021] for solving pfwCSP constraints with non-emptinessconstraints and adopted it as our backend pfwnCSP solver (invoked in Lines 2, 9, 10, and 20). For
optimization problems that only involve maximization, OptPCSat supports 3 different modes:
no-side-condition mode, non-trivial mode, and non-vacuous mode. In the no-side-condition mode,
OptPCSat solves the given CHC optimization problem as it is. In the non-trivial and the nonvacuous modes, OptPCSat finds an optimal solution of the given CHC constraints extended withside-conditions: the two modes require any ordinary predicate variable to be non-empty andthe non-vacuous mode further requires the body of any definite clause to be non-empty. These
additional conditions have been observed in the literature [Albarghouthi et al. 2016; Prabhu et al.
2021] to improve the “usefulness” of synthesized specifications. It is easy to extend Algorithm 1 to
CHC with additional non-emptiness constraints (only for the maximization mode): we enforce theinitial solution obtained in Line 2 of Algorithm 1 to satisfy the side-conditions, and the remaining
optimization steps preserve the conditions. OptPCSat also supports the best-effort optimization
within a specified time limit: it returns the best solution found so far when the time limit is exceeded:
It happens if an initial solution is obtained in Line 2 but the call to Aux does not return, repeatedly
obtaining improved solutions or waiting for a return of the parallel calls to Solve. OptPCSat
returns “Fail” if it fails to obtain an initial solution within the time limit.
We tested OptPCSat on (1) the benchmark set consisting of 65 CHC maximization problems,originally introduced to evaluate HornSpec [Prabhu et al. 2021], and (2) a new benchmark set
consisting of 10 CHC optimization problems to further differentiate our method with related
ones compared in Section 2. The set includes 7 new CHC maximization problems that work as
counterexamples against the soundness of the maximality checking method for HornSpec: Since
14 Following [Unno et al. 2021], we actually use more complicated templates, supporting piecewise linear ranking functions

and lexicographic ordering.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Time in seconds (600 seconds time limit)

Optimal CHC Solving via Termination Proofs

21:25

OptPCSat/No-Side-Condition
HornSpec
OptPCSat/Non-Trivial
OptPCSat/Non-Vacuous
102

101

100

0
10
20
30
40
50
60
70
Benchmarks where an optimal solution was synthesized (out of 72)

Fig. 5. Cactus plot for the experiments on 72=(65+7) CHC maximization problems

it (incorrectly) checks for maximality whether any one-point extension of the current solution
violates the given CHC constraints, to fool HornSpec, each of the 7 problems is designed to haveat least one non-maximal solution whose any one-point extension becomes a non-solution. The
benchmark set also contains the CHC optimization problem obtained from the running programin Section 2 that cannot in principle be solved by the maximal specification synthesis method
based on repeated multi-abduction [Albarghouthi et al. 2016]. Other 2 benchmarks involve bothmaximization and minimization, and hence beyond the scope of the existing methods.
The experiments were conducted on Amazon Linux 2, Intel(R) Xeon(R) Platinum 8259CL CPU@ 2.50GHz CPU and 32 GiB RAM. The time limit was 600 seconds. The experiment results on
CHC maximization benchmarks are summarized as the cactus plot in Figure 5. Out of 72 (=65 + 7)
benchmarks, OptPCSat obtained 59 optimal solutions and 12 (possibly non-optimal) solutions in
the no-side-condition mode. In the non-trivial mode, our tool obtained 54 optimal solutions and17 (possibly non-optimal) solutions. In the non-vacuous mode, OptPCSat obtained 39 optimal
solutions and 26 (possibly non-optimal) solutions. We observed that OptPCSat “failed” more withthe additional non-vacuity and non-triviality conditions because they added an extra overhead on
Solve (Lines 2,12). We also found that the performance decrease was mainly due to the strategy
adopted for synthesizing non-empty predicates, which is again orthogonal to our optimality
checking method. Overall the experimental results show that our optimization method can indeed
find optimal solutions for non-trivial CHC optimization problems, despite the theoretical hardnessof the class of problems. It is also worth mentioning here that initial solutions found by PCSat
were often not optimal and required refinements: the median, minimum, and maximum values of
the numbers of refinements in the no-side-condition mode are 2, 0, and 19. The percentage of the
optimal solutions that never required refinement is 24%. The same numbers in the non-trivial modeare 2, 0, 17, and 14%. In the non-vacuous mode, the numbers are 2, 0, 19, and 25%.
The cactus plot also compares OptPCSat and HornSpec. HornSpec returned solutions for
57 (out of 72) instances. The plot shows that HornSpec is generally faster than OptPCSat asProc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:26

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

expected: note here that we cannot directly compare the results of OptPCSat and HornSpec since
HornSpec does not construct a certificate of the optimality of the returned solution, which is instark contrast to OptPCSat that consumes time for constructing such a certificate in the form of
ordinary, well-founded, functional, and non-empty predicates.
We then have applied OptPCSat to check the optimality of the 57 solutions returned by HornSpec. OptPCSat has successfully shown that 47 solutions are optimal and 2 solutions are nonoptimal. The optimality of the other 8 solutions is unknown. The non-optimal solutions returnedby HornSpec are for 2 problem instances from the new 7 CHC maximization problems that aredesigned to work as counterexamples for HornSpec. That said, HornSpec efficiently found maximal solutions (but without a certificate) for at least 47 (out of 65) problems from the original
benchmark set for HornSpec. It is therefore an interesting future work to combine the approachesof OptPCSat and HornSpec to complement each other.
We conclude this section by discussing the results on the new benchmark set designed todifferentiate OptPCSat from the other related tools. For the new 7 CHC maximization problems,
OptPCSat obtained maximal solutions for 6 problems. The problem instance that OptPCSat was
not able to solve required synthesis of a predicate that involves integer modulo operators that did
not appear in the original constraint set. By manually providing the predicate, OptPCSat solved
the instance, Thus, the failure is not due to a limitation of our optimality checking method but thepredicate synthesis engine of the backend solver PCSat. PCSat successfully solved the other 3
problems: 1 problem that encodes the verification example discussed in Section 1 and 2 problems
that involve both maximization and minimization.
8

RELATED WORK

Sections 2 to 4 have discussed subclasses of CHC optimization and existing optimization methods [Albarghouthi et al. 2016; Hashimoto and Unno 2015; Prabhu et al. 2021; Zhou et al. 2021] indetails. This section compares our work with these work from different perspectives and with otherrelated work.
Optimality beyond Linear-Time Safety. For modular verification of open programs, the usefulnessof angelic non-determinism has been observed by various researchers in the context of angelic
verification [Blackshear and Lahiri 2013; Das et al. 2015; Lahiri et al. 2020], necessary precondition
inference [Cousot et al. 2013], and refinement type optimization [Hashimoto and Unno 2015].
These methods however do not guarantee the semantic optimality of synthesized specifications. By
incorporating their ideas, our approach could be extended, for example, to synthesize a maximallyweak precondition for the non-termination of the given program and to synthesize maximal
specifications of blackbox library functions under an angelic interpretation of non-determinism
exhibited by the target program. To this end, our approach needs to be extended to optimizationof pCSP (resp. CHCs with functionality constraints) for finitely (resp. infinitely) branching nondeterminism. [Hashimoto and Unno 2015] has also discussed synthesis of syntactically-optimal
liveness specifications. We expect that synthesis of liveness specifications with semantic optimality
is within our reach by extending our approach to optimization of CHCs with well-foundedness
constraints.
Existentially quantified CHCs vs. CHCs with non-emptiness. Hashimoto and Unno [2015] reduces
non-optimality checking to satisfiability checking of existentially quantified CHCs [Beyene et al.
2013]. By contrast, we reduce non-optimality to CHCs with non-emptiness constraints, which isexact (i.e. Σ02 -complete), while existentially quantified CHCs is hard. This suggests that focusing on
CHCs with non-emptiness may be beneficial in practice.
Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

Optimal CHC Solving via Termination Proofs

21:27

Multi-Abduction vs. CHC Optimization. Zhou et al. [2021] reduces a maximal specification synthesis problem of library functions invoked from the given recursive function with a postcondition
𝜙 to a multi-abduction problem instead of CHC optimization. Their method thus amounts to synthesizing maximally-weak postconditions of the library functions that make the postcondition 𝜙 to
be an inductive invariant. By contrast we properly reduce maximal specification synthesis to CHC
optimization.
Prabhu et al. [2021] proposed a method for CHC maximization. We have mentioned the incorrectness of their maximality checking algorithm, and here we discuss other aspects of their work.
Their paper proposed a notion of non-vacuous solutions, as a formal criterion for a “practicallyuseful” solution, and developed heuristic methods for efficiently constructing non-vacuous andweak (i.e. close to maximal) solutions. These contributions, which are independent of the flaw in the
maximality checking algorithm, are actually complementary to our development: The combinationof their efficient candidate solution construction method and our correct maximality checker would
provide us with an efficient CHC optimization tool with maximality guarantee. Although theirmaximality checking algorithm is incorrect, the experimental results show that their tool often
returns a maximal solution (of which maximality is automatically provable by our tool) at least for
their benchmark set.
9

CONCLUSION

We presented a computational theoretic analysis of CHC optimization and its subclasses, and basedon the observations, developed a new CHC optimization method that addressed the unsoundness
and the incompleteness of existing predicate constraint optimization methods: our method cansoundly and completely guarantee the semantic optimality of synthesized specifications with respect
to the user-specified preference order via automated termination proofs. Besides the theoreticaldevelopments, we worked toward a practical application to optimal specification synthesis andobtained promising experimental results. Interesting future directions include an extension to
pfwnCSP optimization, which enables optimal synthesis of not only linear-time safety specifications
but also branching-time and/or liveness specifications of non-deterministic programs.
ACKNOWLEDGMENTS
We thank anonymous reviewers for useful comments. This work was supported by JSPS KAKENHI
Grant Numbers JP20H05703, JP22H03564, JP20H04162, JP22H03570 and JP19H04084.
REFERENCES
Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. 2016. Maximal Specification Synthesis. In POPL ’16 (St. Petersburg, FL,
USA). ACM, 789–801.
Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional Rankings, Program Termination,
and Complexity Bounds of Flowchart Programs. In SAS ’10 (Perpignan, France). Springer, 117–133.
Amir M. Ben-Amram and Samir Genaim. 2014. Ranking Functions for Linear-Constraint Loops. J. ACM 61, 4, Article 26(July 2014), 55 pages.
Amir M. Ben-Amram and Samir Genaim. 2017. On Multiphase-Linear Ranking Functions. In CAV ’17. Springer, 601–620.
Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A Constraint-based Approach toSolving Games on Infinite Graphs. In POPL ’14 (San Diego, California, USA). ACM, 221–233.
Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In
CAV ’13 (LNCS, Vol. 8044). Springer, 869–882.
Sam Blackshear and Shuvendu K. Lahiri. 2013. Almost-Correct Specifications: A Modular Semantic Framework for Assigning
Confidence to Warnings. In PLDI ’13 (Seattle, Washington, USA) (PLDI ’13). ACM, 209–218.
Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear Ranking with Reachability. In CAV ’05 (LNCS, Vol. 3576).
Springer, 491–504.

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.

21:28

Yu Gu, Takeshi Tsukada, and Hiroshi Unno

Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI ’06. ACM,
415–426.
Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. 2013. Automatic Inference of Necessary
Preconditions. In VMCAI ’13. Springer, 128–148.
Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. 2015. Angelic Verification: Precise Verification Modulo Unknowns.
In CAV ’15. Springer, 324–342.
Grigory Fedyukovich, Yueling Zhang, and Aarti Gupta. 2018. Syntax-Guided Termination Analysis. In CAV ’18 (LNCS,
Vol. 10981). Springer, 124–143.
Juergen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel,
Carsten Otto, Martin Pluecker, Peter Schneider-Kamp, Thomas Stroeder, Stephanie Swiderski, and Rene Thiemann. 2017.
Analyzing Program Termination and Complexity Automatically with AProVE. Journal of Automated Reasoning 58 (2017),
3–31.
Laure Gonnord, David Monniaux, and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. In PLDI ’15 (Portland, OR, USA). ACM, 608–618.
Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS ’15 (LNCS,
Vol. 9291). Springer, 199–216.
Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs.
In CAV ’14. Springer, 797–813.
Satoshi Kura, Hiroshi Unno, and Ichiro Hasuo. 2021. Decision Tree Learning in CEGIS-Based Termination Analysis. In CAV’21. Springer, 75–98.
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic Termination Verification forHigher-Order Functional Programs. In ESOP ’14 (LNCS, Vol. 8410). Springer, 392–411.
Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob
Lichtenberg, and Chetan Bansal. 2020. Angelic Checking within Static Driver Verifier: Towards high-precision defects
without (modeling) cost. In FMCAD ’20. IEEE, 169–178.
Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL
’01. ACM, 81–92.
Jan Leike and Matthias Heizmann. 2014. Ranking Templates for Linear Loops. In TACAS ’14 (LNCS, Vol. 8413). Springer,
172–186.
Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-Driven Precondition Inference with Learned Features. In
PLDI ’16. 42–56.
Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In
VMCAI ’04 (LNCS, Vol. 2937). Springer, 239–251.
Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, and Deepak D’Souza. 2021. Specification Synthesis with
Constrained Horn Clauses. In PLDI ’21 (Virtual, Canada). ACM, 1203–1217.
Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivančić, and Aarti Gupta. 2008. Dynamic Inference of Likely Data
Preconditions over Predicates by Tree Learning. In ISSTA ’08 (Seattle, WA, USA) (ISSTA ’08). ACM, 295–306.
Yuki Satake, Hiroshi Unno, and Hinata Yanagi. 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI ’20
34, 02 (Apr. 2020), 1644–1651.
Mohamed Nassim Seghir and Daniel Kroening. 2013. Counterexample-Guided Precondition Inference. In ESOP ’13. Springer,
451–471.
Raymond M. Smullyan. 1968. First-order logic. Springer. xii+158 pages.
Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketchingfor Finite Programs. In ASPLOS XII (San Jose, California, USA). ACM, 404–415.
Saurabh Srivastava and Sumit Gulwani. 2009. Program verification using templates over predicate abstraction. In PLDI ’09(Dublin, Ireland). ACM, 223–234.
Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In CAV ’21. Springer,
742–766.
Caterina Urban. 2013. The Abstract Domain of Segmented Ranking Functions. In SAS ’13 (LNCS, Vol. 7935). Springer, 43–62.
Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. In
TACAS ’16. Springer, 54–70.
Caterina Urban and Antoine Miné. 2014. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In ESOP ’14.
Springer, 412–431.
Zhe Zhou, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan. 2021. Data-Driven Abductive Inference ofLibrary Specifications. Proceedings of the ACM on Programming Languages 5, OOPSLA, Article 116 (Oct. 2021), 29 pages.

Received 2022-07-07; accepted 2022-11-07

Proc. ACM Program. Lang., Vol. 7, No. POPL, Article 21. Publication date: January 2023.