{'fraction_non_alphanumeric': 0.041507896565772764, 'fraction_numerical': 0.009226639825532628, 'mean_word_length': 4.301486469317749, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions

Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that formulate verifying safety of programs with bounded iteration and recursion. They both formulate bounded verification problems and are generated by solvers that attempt to verify safety of unbounded iterative or recursive systems. Efficient solvers of recursion-free systems reduce the problem to solving a series of systems that can each be solved tractably. In this paper, we define a novel tractable class of recursion-free systems, named Clause-Dependence Disjoint (CDD) systems, that strictly generalizes tractable classes defined in previous work. We implemented a novel solver for recursion-free CHCs, named Shara, that reduces the problem of solving a given recursion-free system to solving an equivalent CDD system. Our evaluation of Shara on standard benchmarks indicates that, in many practical cases, it performs significantly better than a state-of-the-art implementation.


Introduction
Several critical problems in system verification, such as the verification of safety properties of sequential recursive programs and concurrent programs, can be reduced to solving systems of Constrained Horn Clauses (CHCs), a class of logicprogramming problems [4,6,19,20]. A CHC consists of a body of applications of uninterpreted relational predicates, a constraint in a first-order theory, and a head application of a relational-predicate. A CHC system consists of a set of CHCs and a query relational predicate. A solution of a system is an interpretation of each relational predicate as a formula such that each clause body with predicate symbols substituted with their interpretation entails the interpreted clause head.
Recursive CHC systems can formulate the problem of determining safety of recursive or iterative programs; thus, developing effective solvers for such systems would have wide-reaching applications in verification. However, recursion-free CHC systems, in which each relational-predicate R does not occur in a derivation (i.e., is not a dependency) of itself, are of great interest, both in their own right and in their relationship to recursive systems. First, solving recursion-free systems formulates proving safety of hierarchical programs [14,15], i.e., programs with control branches and procedure calls, but only bounded iteration and recursion.
Second, modern solvers for recursive CHC systems, given a recursive system S, will typically attempt to solve S by constructing a series of recursion-free systems from bounded unwindings of S, solving each of the recursion-free systems, and combining the solutions to construct a solution of S [4]. The performance of the solver for recursive systems critically depends on the performance of the solver for recursion-free systems that it uses.
Many modern CHC solvers, given a recursion-free CHC system S, solve S by solving a series of CHC systems whose combined derivations are the derivations of S, and each of which is a member of a tractable class of systems. The performance of a CHC solver typically is directly determined by how many such systems it must solve and its performance in solving each such system. Previous work has proposed multiple classes of CHC systems that each have a solver which, given a system S in the class, solve S by interpreting each relational predicate in S as an interpolant of two formulas: (1) a Boolean combination of interpretations of relational predicates already found and constraints in S; (2) a Boolean combination of constraints in clauses of predicates in S that are currently unsolved. In the worst case, such solvers can use a prohibitive amount of time, because each interpolant used as an interpretation may have size exponential in the size of the formulas used to construct it. In practice, such solvers typically perform well, because the interpolants generated by practical interpolating theorem provers are typically close to the size of given formulas. We refer to such classes of systems as directly solvable.
Previous work has introduced classes of directly solvable systems that represent different classes of derivations. In particular, previous work has proposed CHC solvers that generate and solve (1) individual derivation trees of a CHC system [11,4,18], (2) body-disjoint systems, which represent multiple derivation trees with a single disjunctive tree system [19,20], and (3) linear CHC systems, which can compactly represent multiple linear derivations with a single system structured as a Directed Acyclic Graph (DAG) [1]. The class of body-disjoint systems strictly contains the class of derivation trees, and is independent of the class of linear systems (i.e., the classes overlap, and neither contains the other) [19,20]. In addition to developing a solver for each class of directly solvable systems, solvers developed in previous work include heuristics that attempt to solve a given recursion-free CHC system S without enumerating and explicitly solving CHC systems with all of the derivations of S.
The main contribution of this paper is the introduction of a novel class of directly-solvable recursion-free CHC systems that strictly contains the union of the classes of body-disjoint and linear systems. In particular, the class consists of all CHC systems such that, for each clause C, the dependences of all distinct relational predicates in C are disjoint; we thus refer to such systems as Clause-Dependent Disjoint (CDD) systems. We present a symbolic algorithm that demonstrates that the class is directly solvable.
The second contribution of this paper is a novel solver for recursion-free CHC systems, named Shara. Shara, given recursion-free system S, reduces the problem of solving S to solving an equivalent CDD system S ′ . The size of S  Fig. 2: Dependencies of CHC system S MC , depicted as a hypergraph. Each relational predicate is a node (circle) and each clause is a hyperedge (box). may be exponential in the size of S, in general. In our experience, the size of S ′ is usually close enough to the size of S for Shara to perform significantly better than the best known CHC solvers. The procedure implemented in Shara to construct S ′ is a generalization of existing procedures for generating compact verification conditions of hierarchical programs [7,14].
We implemented Shara within the Duality CHC solver [4], which is implemented within the Z3 automatic theorem prover [5]. We evaluated the effectiveness of Shara on standard benchmarks drawn from SVCOMP15 [8]. The results indicate that in a strong majority of practical cases, Shara performs better than modern solvers. The results indicate that solvers that perform better than both modern solvers and Shara could be designed by combining the strengths of both approaches (discussed in §5).
The rest of this paper is organized as follows. §2 illustrates the operation of Shara using an example hierarchical program and corresponding CHC system. §3 reviews technical work on which Shara is based. §4 describes Shara in technical detail. §5 gives the results of our empirical evaluation of Shara. §6 compares Shara to related work.

Overview
2.1 Verifying multiCall: an example hierarchical program We will describe Shara by illustrating how it solves a recursion-free CHC system that formulates verifying the safety of the program multiCall (Figure 1). multiCall includes a procedure dbl that, given an integer bound to variable n, returns the value of n doubled (line 1). main, the entry procedure of multiCall, given integer n (line 3), first binds variable res to 0 (line 4). main then tests if n is greater than or equal to 0 (line 5). If so, main doubles the value in n and binds the result to res (line 6). If not, main doubles the value in n, negates the result, and binds the final result to res (line 8). main then returns the value stored in res (line 9).
The problem that we address in this work, in the context of multiCall, is to verify that for each input, multiCall returns a value greater than or equal to 0.
Verifying that multiCall satisfies such a property can be reduced to solving a recursion-free CHC system over a set of relational predicates R[MC] that contains each control location and procedure name in multiCall. A solution interprets each control location L as a summary that relates the arguments in each active call of the function containing L to the program state at L, and interprets each procedure name f as a summary of f. For each step of multiCall to L, there is a corresponding clause with head predicate L. For each procedure f, there is a clause relating state at return locations of multiCall to a summary of their procedure. In particular, one such system S MC is dbl(n, 2 · n) L3(n) =⇒ L4(n, 0) L4(n, res), dbl(n, res ′ ), n ≥ 0 =⇒ L9(n, res ′ ) (1) L4(n, res), dbl(n, res ′ ), n < 0 =⇒ L9(n, −res ′ ) (2) L9(n, res) =⇒ main(n, res) main(n, res), res < 0 =⇒ Err() While S MC has been presented as the result of a translation from hierarchical program multiCall, Shara is purely a solver for CHC systems: it does not require access to the concrete representation of a program, or for a given CHC system to be the result of translation from a program at all. Competitive solvers of recursion-free CHC systems reduce the problem of solving a given CHC system S to solving multiple systems, constructed as copies of sub-systems of S, each of which is directly solvable (as described in §1). In particular, CHC solvers based on tree interpolation reduce solving S to solving copies of subsystems of S in which each relational predicate in S is the head of at most one clause [4,11]. Such systems do not include S MC , which contains multiple clauses with the same head.
As a result, CHC solvers that synthesize tree interpolants may, in the worst case, solve systems that correspond to each derivation of a given CHC system. Such solvers, given S MC , would solve it by generating two tree-interpolation problems, one of which corresponds to the then branch of multiCall and the other which corresponds to the else branch of multiCall. CHC solvers have been proposed which can in many cases avoid enumerating and solving all derivation trees of a given recursion-free system [18]. However, such solvers may enumerate all derivations of a given system in the worst case.
CHC solvers that synthesize disjunctive interpolants reduce solving a given recursion-free system to solving a series of CHC systems in which each relational predicate occurs in the body of at most one clause, and occurs in the body of such a clause at most once; such systems are referred to as body-disjoint systems [19,20]. However, such systems cannot compactly model a program with multiple control paths that share a common subpath, typically modeled as a CHC system with a relational predicate that occurs in multiple clauses (i.e., a relational predicate that is shared ). E.g., S MC is not a body-disjoint system because the relational predicates L4 and dbl occur in both clauses Eqn. 1 and Eqn. 2.
CHC solvers that solve body-disjoint systems, given such a system, generate multiple copies of sub-systems that constrain shared relational predicates. Such a solver, given S MC , generates a body-disjoint system consisting of multiple copies of the subsystems with head relational predicates L4 and dbl.
CHC solvers that synthesize DAG interpolants [1] reduce the problem of solving a given CHC system to solving a series of systems in which each clause contains at most one relational predicate (i.e., linear systems). However, such systems cannot directly model the control flow of a program that contains procedure calls, such as multiCall. Calls can only be compactly modeled using non-linear clauses, such as clauses Eqn. 1 and Eqn. 2.
CHC solvers that solve linear systems, given an arbitrary recursion-free system S, effectively inline constraints on relational predicates that occur in non-linear clauses of S [2]. Such approaches can, in general, generate an inlined system that is exponentially larger than a given system.

multiCall as a Clause-Dependent Disjoint system
Shara, given S MC , solves it directly by issuing a series of interpolation queries, each of which generates an interpretation for a relational predicate in S MC . The key observation behind the design of Shara is that for CHC system S, if the dependences of each relational predicate in each clause of S are disjoint (in which we case we say that S is Clause-Dependent-Disjoint (CDD)), then S is directly solvable. The formal definition of CDD and its key properties are given in §4.1.
E.g., S MC is CDD because for each clause C of S MC , the dependences of all distinct relational predicates in the body of C are disjoint. In particular, for clauses Eqn. 1 and Eqn. 2, the dependences of relational predicates L4 and dbl are disjoint. Figure 2 contains a hypergraph H MC that depicts the dependences induced by the clauses of S MC . The fact that S MC is CDD corresponds to the fact that no node in H MC reaches distinct sources of a common hyperedge.
A solution of an arbitrary CDD system S can be constructed from the results of a series of interpolation queries, each one issued to find an interpretation of a relational predicate of S in order of dependences between relational predicates. For relational predicate R in S, the interpretation of R is the interpolant of two formulas: (1) a Boolean combination of the interpretations found for each dependence of R in S and constraints in S and (2) a Boolean combination of constraints that occur in S.
The performance of the solver is thus largely determined by the ability of the interpolating theorem prover that it uses (1) to generate interpolants quickly and (2) to generate interpolants of size close to that of their input formulas. In the worst case, all interpolating theorem provers given in previous work may use exponential time to generate interpolants of size exponential in the size of their inputs. However, when given formulas that model practical verification problems, modern theorem provers generate interpolants efficiently, which have size close to the size of the given formulas.
E.g., when solving S MC , Shara generates interpretations of relational predicates in the order L3, L4, dbl, L9, and main. It generates an interpretation of L9 in particular as the interpolant of (1) a pre-formula, constructed as a Boolean combination of interpretations generated for L4, dbl and the constraints in Eqn. 1 and Eqn. 2 and (2) a post-formula constructed from constraints in S MC that model the steps of execution of multiCall following 9. A procedure for solving a CDD system directly is given in §4.2.
The class of CDD systems strictly contains all directly-solvable classes introduced in previous work, but does not contain all recursion-free systems. E.g., a recursion-free system that models multiCall mutated to call dbl in sequence, instead of in alternate branches, would not be CDD. Shara, given an arbitrary recursion-free CHC system S, solves it by generating an equivalent CDD system S ′ and solving S ′ directly. In general, S ′ may have size exponential in the size of S. In practice, a suitable equivalent system can be generated using heuristics analogous to those used to generate compact verification conditions of hierarchical programs [7,14]. A general procedure for constructing a CDD expansion of a given CHC system is given in §A.

Logical interpolation
Shara solves CHC systems, logic-programming problems in which a solution maps predicate symbols to first-order formulas. All objects defined in this paper are defined over a fixed space of logical variables X. In particular, for theory T , the space of T formulas over X is denoted For sequences of variables Y = [y 0 , . . . , y n ] and Z = [z 0 , . . . , z n ], the T formula constraining the equality of each element in Y with its corresponding element in Z, i.e., the formula 0≤i≤n An interpolant of mutually inconsistent T formulas φ 0 and φ 1 is a T formula in their common vocabulary that explains their inconsistency.
All spaces of formulas in the remainder of this paper will be defined for a fixed, arbitrary theory T that supports interpolation, such as combinations of the theories of linear arithmetic and the theory of uninterpreted functions with equality. Although determining the satisfiability of formulas in such theories is NP-complete in general, decision procedures [5] and interpolating theorem provers [16] for such theories have been proposed that operate on such formulas efficiently. Shara is defined as using a decision procedure for T named IsSat, and an interpolating theorem prover for T named Itp.

Constrained Horn Clauses
Structure A Constrained Horn Clause is a body, consisting of a conjunctive set of uninterpreted relational predicates and a constraint, and a head relational predicate. Relational predicates are predicate symbols paired with a map from each symbol to its arity.
Definition 2 For each space of symbols R and function a : The space of all relational predicates is denoted Preds. For each space of relational predicates R ∈ Preds, we denote the predicate symbols and arity of R as Rels R and Arity R , respectively. For relational predicates R ∈ Preds and symbol R, we denote R ∈ Rels R alternatively as R ∈ R. All definitions introduced in this section are given over a fixed, arbitrary set of relational-predicate symbols R.
An application of a relational predicate is a relational-predicate symbol R paired with a sequence of variables of length equal to the arity of R.
The space of applications is denoted Apps R . For each application A ∈ Apps R , the predicate symbol and argument sequence of A are denoted Rel[A] and Args[A] respectively.
A Constrained Horn Clause is a body of applications, a constraint, and a head application. We will present Shara as a solver for CHCs without recursive definitions of predicates, represented in a normalized form. In particular, for C ∈ CHC[R], let the dependence relation of C, denoted Deps C , be Let S ⊆ CHC[R] be such that (1) each relational predicate occurs in the head of some clause, (2) each R ∈ R is applied to the same variables Vars S (R) in each of its occurrences in a clause as a head, (3) all clauses with distinct head relational predicates are defined over disjoint spaces of variables, and (4) there is exactly one relational predicate Query S that is the dependency of no relational predicate. Then S is a normalized recursion-free system. For the remainder of this paper, we consider only normalized sets of CHCs, and denote the space of such sets as CHCs[R].
Solutions A solution to a CHC system S is an interpretation of each relational predicate R of arity n as a formula over n free variables such that for each clause C ∈ S, the conjunction of interpretations of all relational predicates in the body of C and the constraint of C entail the interpretation of the head of C. Let a map from each R ∈ Rels R to a formula over an ordered vector of Arity R (R) free variables be an interpretation of R; let the space of interpretations of R be denoted Interps R .
Definition 5 For B ∈ Bodies R and H ∈ Apps R , let σ ∈ Interps R be such that for each R ∈ R, Arity R (R) = deg(σ(R)) and
For S ∈ CHCs[R], if (a) for each R ∈ Dom(σ) (where Dom(σ) denotes the domain of σ) and R ′ ∈ R a dependence of R in S, it holds that R ′ ∈ Dom(σ); (b) for each C ∈ S such that Rel[Head C ] ∈ Dom(σ), σ is a solution of C; then σ is a partial solution of S. If, in addition, σ(Query S ) |= False, then σ is a solution of S. The problem addressed in this paper is, given a recursion-free CHC system S, to synthesize a solution for S.
Each partial solution σ of S defines a simpler CHC system in which each relational predicate in the domain of σ is replaced with its interpretation in σ. For A ⊆ Apps R , φ ∈ Forms, and σ ∈ Interps R , the clause body For each S ∈ CHCs[R] and σ ∈ Interps R a partial solution of S, the grounding of S on σ is a CHC system in which each clause is a grounding of a clause in S with a head relational predicate not in the domain of σ. In particular, let S ′ ⊆ CHC[R \ Dom(σ)] be such that for each B ∈ Bodies R and H ∈ Apps R with Rel[H] / ∈ Dom(σ), the clause (σ(B), H) is in S ′ . Then S ′ is the grounding of S on σ, denoted σ(S).

Technical Approach
This section presents the technical details of our approach. §4.1 presents the class of Clause Dependent Disjoint systems and its key properties. §4.2 describes how Shara solves CDD systems directly. §4.3 describes how Shara solves a given recursion-free system by solving an equivalent CDD system. Proofs of all theorems stated in this section are contained in §B and §C.

Clause-Dependent Disjoint Systems
The key contribution of our work is the introduction of the class of Clause-Dependent Disjoint (CDD) systems. The class of CDD systems is a subclass of the class of recursion-free CHC systems that contains known subclasses of recursion-free systems that can be solved directly, and can itself be solved directly.

Definition 6 For R ∈ Preds and S ∈ CHCs[R]
, if for all R 0 , R 1 ∈ R that are siblings in S ( §3.2), the transitive dependences of R 0 and R 1 in S are disjoint, then S is Clause-Dependence-Disjoint (CDD). CDD systems can model hierarchical programs with branching and procedure calls in which each path of the program calls each procedure at most once.
Example 1 The CHC system S MC (given in §2.2) is a CDD system. The only clauses in S MC that contain multiple relational predicates are Eqn. 1 and Eqn. 2, which both contain L4 and dbl. The dependences of L4 and dbl are disjoint.
The class of CDD systems contains several classes of recursion-free systems introduced in previous work. For recursion-free system S, if each relational predicate R that occurs in S occurs in the body of at most clause of S, and occurs in each clause at most once, then S is body-disjoint [19,20]. If the body of each clause in S contains at most relational predicate, then S is linear [1].

Theorem 1
The class of CDD systems strictly contains the union of the classes of body-disjoint and linear systems.
The CHC system S MC ( §2.2) is not body-disjoint or linear, but is CDD. A proof that both the classes of body-disjoint and linear systems are contained in the class of CDD systems is given in §B.

Solving a CDD system
For R ∈ Preds, the procedure SolveCdd R (Alg. 1) is a solver for CDD systems in CHCs[R]. SolveCdd R , given S ∈ CHCs[R], defines a procedure SAux that, given a partial solution σ of S, returns an extension of σ that is a solution of S (line 2-line 9). SolveCdd R runs a procedure Cex R that, given a CDD system S ∈ CHCs[R], returns a a formula that is satisfiable if and only if S has no solution, which we refer to as a counterexample characterization of S (line 10; the implementation of Cex R is given below). SolveCdd R runs IsSat ( §3.1) Input : For R ∈ Preds, a CDD system S ∈ CHCs[R]. Output : If S is solvable, then a solution of S; otherwise, the value None. 1  Algorithm 1: SolveCdd R : for R ∈ Preds and CDD system S ∈ CHCs[R], returns a solution to S or the value None to denote that S has no solution.
on Cex R (S); if IsSat returns that Cex R (S) is satisfiable, then SolveCdd R returns that S has no solution (line 10). Otherwise, SolveCdd R runs SAux on the empty partial solution and returns the result (line 11). SAux, given partial solution σ, constructs the set R ′ of each relational predicate R such that R is not in the domain of σ and all dependents of R in S are in the domain of σ (line 3). If R ′ is empty, then SAux returns σ as a solution of S (line 5). Otherwise, if there is some R ∈ R ′ (line 6), then SAux extends σ to map R to an interpolant of the formulas Pre R (S, σ, R) and Post R (S, σ, R), defined below. The interpolant of the two formulas is synthesized by running the procedure Itp ( §3.1). SAux recurses on the extended partial solution and returns the result (line 7).

Example 2 SolveCdd R[MC] , given S MC , may generate interpretations of R[MC]
in any topological ordering of the dependency relation of S MC , depending on the relational predicates that it chooses at line 4. One such ordering is L3, L4, dbl, L9, main, Err.

Constructing the Counterexample Characterization of a CDD For T ∈ CHCs[R]
, the formula Cex R (T ) is a compact representation of the counterexample characterization of T , defined as follows. For each R ∈ R, let there be a Boolean predicate Use[R]. The constraint of R, denoted Ctr[R] ∈ Forms, constrains that if R occurs in a derivation of T , then there is some C ∈ T in which R is the head such that (1) each R ′ ∈ R in an application in the body of C is used and (2) the values assigned to each application of R ′ are equal to the values assigned to the head variables of R ′ in T . I.e., Ctr[R] is The counterexample characterization of T constrains that (1) the query predicate of T must be used in a derivation and (2) for R ∈ R, if R is used, then its constraint must hold. I.e., Example 3 Cex R[MC] (S MC ) characterizes all runs of multiCall that result in an error. Although the relational predicates L4 and dbl occur in the bodies of multiple clauses, they are each modeled with only a single instance of logical variables. Such a collection is sufficient because each run of multiCall reaches L4 and dbl at most once. Correspondingly, each derivation of S MC contains at most one occurrence of relational predicates L4 and dbl.
Constructing the pre-constraint of a relational predicate For partial solution σ : R → Forms of S, and R ∈ R for which each dependency is in the domain of σ, the pre-constraint Pre R (S, σ, R) is a formula that is entailed by the interpretation of R in each solution of S that extends σ. In particular, Pre R (S, σ, R) is:

σ(Rel[A])[Args[A]]
  Example 4 Assume that SolveCdd[MC], given S MC , synthesizes a partial solution σ ∈ Interps R[MC] that interprets L3 as True, and chooses to then find an interpretation of L4. The pre-constraint of L4 is True ∧ res 4 = 0, where res 4 is a logical variable that models the value of res at line 4.
Constructing the post constraint of a relational predicate For σ ∈ Interps R a partial solution of S and R ∈ R, the post constraint Post R (S, σ, R) ∈ Forms is mutually inconsistent with the interpretation of R in each solution of S that extends σ. In particular, let D 0 be the reflexive dependents of R in S. Let D 1 be the siblings in S of D 0 . Let D 2 be all dependences of D 1 . Let D = D 0 ∪ D 1 ∪ D 2 . Let S| D be S restricted to clauses whose head's relational predicate is in D. The post constraint for S under σ at R is the counterexample characterization of S| D grounded on σ (defined in §3.2). I.e., Post R (S, σ, R) = Cex R (σ(S| D )).

Solving recursion-free systems using CDD systems
Shara R , given S ∈ CHCs[R], constructs a CDD system S ′ equivalent to S. Shara then directly solves S ′ and from its solution, constructs a solution of S. For R, R ′ ∈ Preds, S ∈ CHCs[R] and S ′ ∈ CHCs[R ′ ], if there is a homomorphism from R ′ to R that preserves the relationship between the clauses of S ′ in the clauses of S, then S ′ is an expansion of S. All definitions in this section will be over fixed R, R ′ , S, and S ′ .
is in S. Then f is a correspondence from S ′ to S.
If there is a correspondence from S ′ to S, S ′ is an expansion of S, denoted S ⪯ S ′ .
Definition 8 If S ′ is CDD, S ⪯ S ′ , and there is no CDD system S ′′ such that S ⪯ S ′′ ⪯ S and S ′′ ̸ = S ′ , then S ′ is a minimal CDD expansion of S.
Shara R (Alg. 2), given S ∈ CHCs[R] (line 1), returns a solution to S or the value None to denote that S is unsolvable. Shara R first runs a procedure Expand R on S to obtain a minimal CDD expansion S ′ ∈ CHCs[Ctxs[R]] (Defn. 8) of S (where Ctxs[R] is a space of relational predicates defined by R, defined in §A), and a correspondence η : Ctxs[R] → R (line 2). Shara R then runs a procedure SolveCdd Ctxs[R] on S ′ , which either returns the value None to denote that S ′ has no solution or a solution σ ′ (line 3). If SolveCdd Ctxs[R] returns that S ′ has no solution, then Shara returns that S has no solution (line 4). Otherwise, if SolveCdd Ctxs[R] returns a solution σ ′ , then Shara returns, as a solution to S, Collapse σ ′ η , defined above (line 5). For σ ∈ Interps Ctxs[R] and correspondence η from S ′ to S, Collapse σ η ∈ Interps R maps each R ∈ R to Theorem 2 S is solvable if and only if Shara R (S) ∈ Interps R .

Evaluation
We performed an empirical evaluation of Shara to determine in what cases Shara performs better or worse than existing solvers for recursion-free CHC systems. To do so, we implemented Shara as a modification of Duality CHC solver, which is included in the Z3 theorem prover [9]. We modified Duality to use Shara as its solver for recursion-free CHC systems. We modified the algorithm used by Duality to generate recursion-free unwindings of a given recursive system so that in each iteration, it generates an unwinding with a maximal set of relational predicates and clauses. In the following context, "Shara" refers to Duality modified to solve general CHC systems.
We evaluated Shara and Duality on 4,309 CHC systems generated from programs in the SV-COMP 2015 [8] verification benchmark suite. To generate CHC systems, we ran the SeaHorn [10] verification framework with its default settings, set to timeout at 90 seconds. We used the benchmakrs in SV-COMP 2015 [8] because they were used to evaluate Duality in previous work [18]. The source code of our implementation of Shara is publicly available [21].
All experiments were run on a machine with 16 1.4 GHz processors and 128 GB of RAM. The evaluated implementations of Shara and Duality each use a single thread. We ran the solvers on each benchmark, timing out each implementation after 180 seconds.
Out of 4,309 benchmarks, Shara solved or refuted 2,408, timed out on 762, and for 1,139 benchmarks, generated a constraint that caused Z3's interpolating theorem prover to fail, which caused Shara to neither be able to solve or refute the CHC system. Duality solved or refuted 2,321 benchmarks, timed out on 1,145, and failed due to an error thrown by Z3's interpolating theorem prover on 843. The two solvers can induce a failure in Z3 on different systems because in attempting to solve a given system, they generate different interpolation queries.
We also attempted to compare Shara to the Eldarica CHC solver, but found that it could not parse the CHC systems generated by SeaHorn. We compared Shara and Eldarica on an alternative set of benchmarks generated by the UFO model checker [3], and found that Shara outperformed Eldarica by at least an order of magnitude on an overwhelming number of cases. As a result, for focus our discussion on a comparison of Shara and Duality.
The results of our evaluation are contained in Figure 3. Of the 4,040 benchmarks on which both solvers took a negligible amount of time-less than five seconds-Shara solved the benchmarks in an average of 0.51 seconds and Duality solved them in an average of 0.42 seconds. Figure 3 contains data on only the benchmarks that were not solved in a negligible amount of time. Out of the 269 non-negligible benchmarks, Shara solved 185 in less time than Duality, and solves 159 in less than half the time of Duality. Duality solved 84 in less time than Shara, and solved 53 in less than half the time of Shara. Of the 762 benchmarks on which Shara timed out, Duality solved or found a counterexample to 185. Of the 1,145 benchmarks on which Duality timed out, Shara solved or found a counterexample to 470.   Figure 4 shows the relationship between the solving times of Duality and Shara and the size of a given system, measured as lines of code in the format generated by SeaHorn. Because the majority of files have size ranging between 1,000 and 100,000, Figure 4 is restricted to this range to clarify the presentation. The data indicates that that performance improvement of Shara compared to Duality is consistent across systems of all sizes available.
The results indicate that (1) on a significant number of verification problems, Shara can perform significantly better than Duality, but (2) there are some cases in which the strengths of each algorithm yield better results. We collected the differences between sizes of a given system and its minimal CDD expansion generated by Shara and found that they were independent of Shara's performance compared to Duality. Thus, while Duality may in the worst case enumerate exponentially many derivation trees, it appears to enumerate a number much lower than the worst-case bound in some cases, causing it to perform better than Shara. Our results indicate that a third approach that combines the strengths of both Duality and Shara, perhaps by lazily unwinding a given recursion free system into a series of CDD systems instead of derivation trees, could yield further improvements.

Related Work
A significant body of previous work has presented solvers for different classes of Constrained Horn Clauses, or finding inductive invariants of programs that correspond to solutions of CHCs. Impact attempts to verify a given sequential procedure, which corresponds to solving a recursive linear CHC system [17]. Impact attempts to verify a given procedure by iteratively selecting paths and synthesizing invariants for each path. Such an approach corresponds to iteratively and selecting and solving derivations of a corresponding linear CHC system.
Previous work also proposed a verifier for recursive programs [11], which corresponds to solving recursive CHC systems. The proposed approach selects interprocedural paths of a program and synthesizes invariants for each as nested interpolants. Such an approach corresponds to attempting to solve a recursive CHC system S by selecting derivation trees of S and solving each tree.
Previous work has proposed solvers for recursive systems that, given a system S, attempt to solve S by generating and solving a series of recursion-free unwindings of S. In particular, Duality attempts to solve each unwinding S ′ by selecting and solving derivation-trees of S ′ [4]. An optimized version of Duality selects derivation trees to solve using lazy annotations, a symbolic analog of Prolog evaluation with tabling [18]. Eldarica attempts to solve each recursion-free CHC system by lazily copying its subsystems to form a body-disjoint over-approximation [19,20].
Whale attempts to verify a sequential recursive program by generating and solving hierarchical programs (i.e., programs that may contain conditional branches and procedure calls, but do not contain loops or recursion), which correspond to recursion-free CHC systems [2]. To solve a particular recursionfree system S, Whale generates a linear inlining S ′ of S and solves it using a procedure Vinta [1]. In general, S ′ may have size exponential in the size of S.
Shara is similar to all of the approaches given above for solving recursion-free CHC systems in that it reduces the problem of solving a given recursion-free CHC system S to solving a CHC system in a directly-solvable class. Shara is distinct from all of the approaches given above in that it reduces solving a recursion-free CHC system to solving a Clause-Dependent Disjoint (CDD) system. CDD systems strictly contain the union of all classes of directly-solvable CHC systems used by the above approaches, and can themselves be solved directly.
Previous work has given solvers for non-linear Horn clauses over particular theories. In particular, verifiers have been proposed for recursion-free systems over the theory of linear arithmetic [13]. Because the verifier relies on quantifier elimination, it is not clear if it can be extended to richer theories that support interpolation, such as the combination of linear arithmetic with uninterpreted functions. Other work gives a solver for the class of timed pushdown systems, a subclass of CHC systems over the theory of linear real arithmetic [12]. Unlike both approaches, Shara can solve systems over any theory that supports interpolation.
DAG inlining, given a hierarchical program P , attempts to generate a compact verification condition for P [14]. Shara contains a procedure that, given a recursion-free Horn Clause system S, attempts to construct a compact CDD system S ′ such that each solution of S ′ defines a solution of S. Because hierarchical programs and recursion-free Horn Clauses correspond closely to each other, algorithms that operate on hierarchical programs directly correspond to algorithms that operate on recursion-free Horn Clauses. However, an algorithm for constructing a verification condition of hierarchical programs cannot apparently be directly used to synthesize a solution of a recursion-free CHC system.

A Generating a Minimal CDD Expansion
ExpandR always returns a CDD expansion of its input (see §C, Lemma 3) that is minimal. ExpandR is certainly not unique as an algorithm for generating a minimal CDD expansion. In particular, feasible variations of ExpandR can be generated from different implementations of SharedRel, each of which chooses clause-relations pairs to return based on different heuristics. We expect that other expansion algorithms can also be developed by generalizing algorithms introduced in previous work on generating compact verification conditions of hierarchical programs [14].

B Proof of characterization of CDD systems
The following is a proof of Thm. 1.
Proof. To prove that the union of the classes of linear systems and body-disjoint systems are strictly contained by the class of CDD systems, we prove (1) the class of linear systems are contained by the class of CDD systems, (2) the class of body-disjoint systems are contained by the class of CDD systems, and (3) there is some CDD system that is not linear or body-disjoint.
For goal (1), let S be an arbitrary linear system. S is CDD if for each clause C in S, for each pair of distinct relational predicates in the body of C, the transitive dependencies are disjoint (Defn. 6). Let C be an arbitrary clause in S. C has no pairs of distinct clauses, by the fact that S is linear. Therefore, S is CDD.
For goal (2), let S be an arbitrary body-disjoint system. The dependence relation of S is a tree T , by the definition of a body-disjoint system. Let C be an arbitrary clause in S, with distinct relational predicates R0 and R1 in its body. All dependences of R0 and R1 are in subtrees of T , which are disjoint by the definition of a tree. Thus, S is CDD, by Defn. 6.
For goal (3), the system S MC is CDD, but is not linear or body-disjoint.

C Proof of Correctness
In this section, we give a proof that Shara is a correct solver for recursion-free CHC systems. We first establish lemmas for the correctness of each procedure used by Shara, namely Collapse (Lemma 1 and Lemma 2), ExpandR (Lemma 3), and SolveCddR (Lemma 4, Lemma 6, and Lemma 7). We combine the lemmas to prove correctness of Shara (Thm. 2). For CHC systems S and S ′ , if S ′ is an expansion of S, then the result of collapsing a solution of S ′ is a solution of S. Lemma 1 For R, R ′ ∈ Preds, S ∈ CHCs[R], S ′ ∈ CHCs[R ′ ], σ ′ ∈ Interps R ′ , and η : R ′ → R a correspondence from S ′ to S, Collapse σ ′ η is a solution of S. Proof. Let B ∈ BodiesR, φ ∈ Forms, and R ∈ R be such that ((B, φ), R(VarsS(R))) ∈ S. For each R ′ ∈ R ′ such that η(R ′ ) = R, there is some B ′ ∈ Bodies R ′ such that ((B ′ , φ), R ′ (VarsS(R))) ∈ S ′ , by the fact that S ′ is an expansion of S and the definition of an expansion. σ ′ (B ′ ), φ |= σ ′ (R ′ ) by the fact that σ ′ is a solution of S ′ .
For CHC solvable system S, each expansion of S is solvable.
Lemma 2 For R, R ′ ∈ Preds, S ∈ CHCs[R] such that S is solvable, and S ′ ∈ CHCs[R ′ ] such that S ′ is an expansion of S, S ′ is solvable.
Then σ is a solution of S ′ .
ExpandR always returns a CDD expansion of its input. The inductive fact is that in each step of evaluation ExpAux, CorrR is a correspondence from argument S ′ to S. For the base case, ExpAux is called initially on S, by Alg. 3.
CorrR is a correspondence from S to itself, by the definition of CorrR ( §A). For the inductive case, for C ∈ S and R ∈ Ctxs[R], ExpAux calls itself on CopyRelR(S, C, R). For each S ′ ∈ CHCs[Ctxs [R]] such that CorrR is a correspondence from S ′ to S, CorrR is a correspondence from CopyRelR(S ′ , C, R) to S, by definition of CopyRelR ( §A). By this fact and the inductive hypothesis, CorrR is a correspondence from CopyRelR(S ′ , C, R) to S.
ExpAuxR returns its parameter at some step, by Alg. 3. Therefore, ExpAux returns an expansion of S. Furthermore, ExpandR returns a minimal CDD expansion of its input. This fact is not required to prove Thm. 2, and thus a complete proof is withheld. For each CHC system S, S has a solution if and only if the verification condition of S is unsatisfiable.
Lemma 4 For R ∈ Preds and S ∈ CHCs[R] that is CDD and solvable, CexR(S) is unsatisfiable.
Proof. Assume that S has solution σ and m is a model of CexR(S). There are some relational predicates R ′ ⊆ R containing Query S such that for each R ′ ∈ R ′ , m(Use[R]) holds, by the definition of CexR ( §4.2). For each R ′ , the interpretation of m over Vars R ′ must satisfy σ(R ′ ), by well-founded induction on DepsS restricted to R ′ . But σ(Query S ) = False, by the definition of a solution of a CHC system (Defn. 5). Therefore, there can be no such model m. Therefore, CexR(S) is unsatisfiable.
Lemma 5 For R ∈ Preds and S ∈ CHCs[R] such that CexR(S) is unsatisfiable, SolveCddR(S) is a solution of S.