Andrew Reynolds

Jasmin Christian Blanchette

Morgan Deters

A Decision Procedure for (Co)datatypes in SMT Solvers

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson-Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from formalizations developed with Isabelle demonstrates the potential of the procedure.

Introduction

Freely generated algebraic datatypes are ubiquitous in functional programs and formal specifications. They are especially useful to represent finite data structures in computer science applications but also arise in formalized mathematics. They can be implemented efficiently and enjoy properties that can be exploited in automated reasoners.

 all depend on codatatypes to capture infinite processes.

Codatatypes are freely generated by their constructors, but in contrast with datatypes, infinite constructor terms are also legitimate values for codatatypes (Section 2). Intuitively, the values of a codatatype consist of all well-typed finite and infinite ground constructor terms, and only those. As a simple example, the coalgebraic specification

introduces a type that models the natural numbers Z, S(Z), S(S(Z)), . . ., in Peano notation, extended with an infinite value ∞ = S(S(S(. . .))). The equation S(∞) ≈ ∞ holds as expected, because both sides expand to the infinite term S(S(S(. . .))), which uniquely identifies ∞.

Datatypes and codatatypes are an integral part of many proof assistants, including Agda, Coq, Isabelle, Matita, and PVS. In recent years, datatypes have emerged in a few automatic theorem provers as well. The SMT-LIB [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] format, supported by most SMT (satisfiability modulo theories) solvers, is being extended with a syntax for datatypes. In this article, we introduce a unified decision procedure for universal problems involving datatypes and codatatypes in combination (Section 3). The procedure is described abstractly as a calculus and is composable via the Nelson-Oppen method [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF]. It generalizes the procedure by Barrett et al. [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF], which covers only datatypes.

Datatypes and codatatypes share many properties, so it makes sense to consider them together. There are, however, at least three important differences. First, codatatypes need not be well-founded. For example, the type codatatype stream τ = SCons(τ, stream τ ) of infinite sequences or streams over an element type τ is allowed, even though it has no base case. By contrast, the corresponding datatype specification datatype fstream τ = FSCons(τ, fstream τ ) would be rejected as non-well-founded [START_REF] Blanchette | Witnessing (co)datatypes[END_REF]. Second, a uniqueness rule takes the place of the acyclicity rule of datatypes. Cyclic constraints such as x ≈ S(x) are unsatisfiable for datatypes, thanks to an acyclicity rule, but satisfiable for codatatypes. For the latter, a uniqueness rule ensures that two values having the same infinite expansion are equal; from x ≈ S(x) and y ≈ S(y), it deduces x ≈ y. These two rules are needed to ensure completeness (solution soundness) on universal problems. They cannot be finitely axiomatized, so they naturally belong in a decision procedure. Third, it must be possible to express cyclic (regular) values as closed terms and to enumerate them. This is necessary when generating models. The µ-binder notation associates a name with a subterm; it is used to represent cyclic values in the metatheory and in the generated models. For example, the µ-term SCons(1, µs. SCons(0, SCons(9, s))) stands for the lasso-shaped sequence 1, 0, 9, 0, 9, . . . . Our procedure is implemented in the SMT solver CVC4 [1] as a combination of rewriting and a theory solver (Section 4). It consists of about 2000 lines of C++ code, most of which are shared between datatypes and codatatypes. The code is integrated in the development version of the solver and is expected to be part of the CVC4 1.5 release. An evaluation on problems generated from Isabelle/HOL [START_REF] Nipkow | Isabelle/HOL: A Proof Assistant for Higher-Order Logic[END_REF] formalizations using the Sledgehammer tool [START_REF] Blanchette | Extending Sledgehammer with SMT solvers[END_REF] demonstrates the usefulness of the approach (Section 5).

An earlier version of this article was presented at the CADE-25 conference in Berlin, Germany [START_REF] Reynolds | A decision procedure for (co)datatypes in SMT solvers[END_REF]. This article extends the conference paper with additional background material on (co)datatypes (Section 2), more detailed metatheoretical proofs (Section 3), a description of the generation of models with µ-binders in CVC4 (Section 4), and a more comprehensive evaluation (Section 5).

Related Work. Barrett et al. [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF] provide a good account of related work on datatypes as of 2007, in addition to describing their implementation in CVC3. Since then, datatypes have been added not only to CVC4 (a complete rewrite of CVC3) but also to the SMT solver Z3 [START_REF] De Moura | Z3: An efficient SMT solver[END_REF] in unpublished work by Leonardo de Moura and to a SPASS-like superposition prover by Wand [START_REF] Wand | Polymorphic+typeclass superposition[END_REF]. In his Ph.D. thesis [START_REF] Bjørner | Integrating decision procedures for temporal verification[END_REF], Bjørner introduced a decision procedure for (co)datatypes in STeP, the Stanford Temporal Prover. Closely related are the automatic structural induction in SMT solvers [START_REF] Reynolds | Induction for SMT solvers[END_REF] and superposition provers [START_REF] Cruanes | Extending superposition with integer arithmetic, structural induction, and beyond[END_REF][START_REF] Kersani | Combining superposition and induction: A practical realization[END_REF], the (co)datatype and (co)induction support in Dafny [START_REF] Leino | Co-induction simply-Automatic co-inductive proofs in a program verifier[END_REF], and the (semi-)decision procedures for datatypes implemented in Leon [START_REF] Suter | Satisfiability modulo recursive programs[END_REF] and RADA [START_REF] Pham | RADA: A tool for reasoning about algebraic data types with abstractions[END_REF]. Datatypes are supported by the higher-order model finder Refute [START_REF] Weber | SAT-based finite model generation for higher-order logic[END_REF] for Isabelle. Its successor, Nitpick [START_REF] Blanchette | Nitpick: A counterexample generator for higher-order logic based on a relational model finder[END_REF], can also generate models involving cyclic codatatype values. Cyclic values have been studied extensively under the heading of regular or rational trees-see Carayol and Morvan [START_REF] Carayol | On rational trees[END_REF] and Djellou et al. [START_REF] Djelloul | Theory of finite or infinite trees revisited[END_REF] for recent work. The µ-notation is inspired by the µ-calculus [START_REF] Endrullis | On equal µ-terms[END_REF][START_REF] Kozen | Results on the propositional µ-calculus[END_REF].

Conventions. Our setting is a monomorphic (or many-sorted) first-order logic. A signature Σ = (Y , F ) consists of a set of types Y and a set of function symbols F . Types are atomic sorts and interpreted as nonempty domains. The set Y must contain a distinguished type bool interpreted as the set of truth values. The metavariables δ, ε range over (co)datatypes, whereas τ, υ range over arbitrary types.

Function symbols are written in a sans-serif font (e.g., f, g) to distinguish them from variables (e.g., x, y). Symbol names starting with an uppercase letter (e.g., S) are reserved for constructors. With each function symbol f is associated a list of argument types τ 1 , . . . , τ n (for n ≥ 0) and a return type τ, written f :

τ 1 × • • • × τ n → τ; this notation collapses to f : τ if n = 0.
Functions invocations f(t 1 , . . . , t n ) apply the n-ary function symbol f to n arguments t 1 :τ 1 , . . . , t n : τ n of the right types. Nullary function symbols, also called constants, can appear without parentheses in terms. The set F must at least contain true, false : bool, interpreted as truth values. The only predicate is equality, written ≈; it belongs to the logical symbols. Other predicates can be represented as functions to bool, with p(. . .) abbreviating p(. . .) ≈ true. The notation t τ stands for a term t of type τ; it should not be confused with t : τ, which is a statement expressing that t has type τ. When applied to terms, the standard equality symbol = denotes syntactic equality. The operator i ϕ i abbreviates a conjunction ϕ 1 ∧ • • • ∧ ϕ n . Finally, x abbreviates a list or tuple x 1 , . . . , x n .

(Co)datatypes

We fix a signature Σ = (Y , F ). The types are partitioned into Y = Y dt Y codt Y ord , where Y dt are the datatypes, Y codt are the codatatypes, and Y ord are the remaining ordinary types (which can be interpreted or not). The function symbols are partitioned into F = F ctr F sel , where F ctr are the constructors and F sel are the selectors. There is no need to consider further function symbols because they can be abstracted away as variables when combining theories. Exceptionally, it is convenient to use numeric constants (0, 1, . . . ) in examples. Σ-terms are standard first-order terms over Σ, without µ-binders.

In an SMT problem, the signature is typically given by specifying first the uninterpreted types in any order, then the (co)datatypes with their constructors and selectors in groups of mutually (co)recursive (co)datatypes, and finally any other function symbols. Each (co)datatype specification consists of mutually recursive types that are either all datatypes or all codatatypes. Polymorphic types, nested (co)recursion, and datatype-codatatype mixtures fall outside this fragment. 1 We allow ourselves some notational parameteriza-tion through subscripts-for example, stream τ denotes a family of ground types including stream int , stream bool , and stream stream real .

Each (co)datatype δ is equipped with m ≥ 1 constructors, and each constructor for δ takes zero or more arguments and returns a δ value. The argument types must be either ordinary, among the already known (co)datatypes, or among the (co)datatypes being introduced. To every argument corresponds a selector. The names for the (co)datatypes, the constructors, and the selectors must be distinct and different from existing names. 2 Schematically: Because all types must be inhabited (nonempty), a datatype specification is admissible only if a ground constructor term can be exhibited. This rules out non-well-founded specifications such as that of fstream in Section 1. For codatatypes, no admissibility check is necessary because there is always a term, finite or infinite, that witnesses nonemptiness [START_REF] Blanchette | Witnessing (co)datatypes[END_REF].

(co)datatype δ 1 = C 11 ( s 1 11 : τ 1 11 , . . . , s n 11 11 : τ n 11 11 ) | • • • | C 1m 1 (. . .) . . . and δ = C 1 (. . .) | • • • | C m (. . .) with C ij : τ 1 ij × • • • × τ n ij ij → δ i and s k ij : δ i → τ k ij .
A type δ depends on another type ε if ε is the type of an argument to one of δ's constructors. Semantically, a set of types is mutually (co)recursive if and only if the associated dependency graph is strongly connected. A type is (co)recursive if it belongs to such a set of types. Types can be declared together in a mutual fashion even if they are not actually mutually (co)recursive. The semantic notion is more precise and is the one that interests us.

Non(co)recursive type specifications such as either of datatype option τ = None | Some(τ) codatatype complex = Complex(re: real, im: real) are permitted. At the semantic level, it makes no difference whether such types are introduced as datatypes or as codatatypes.

One way to characterize datatypes is as the initial model of the selector-constructor equations [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF]. A drawback of this approach is that it does not naturally account for selectors applied to wrong constructors. Barrett et al. address this by parameterizing the construction by default values, but this gives rise to spurious equalities between unrelated terms. For example, given

datatype x = C(s: int) | D | E
we would have the spurious equality s(D) ≈ s(E). This flaw could be corrected, but the added complexity seems to suggest that selectors are better characterized axiomatically.

A related semantic view of datatypes is as initial algebras of suitable functors. Codatatypes are then defined dually as final coalgebras [START_REF] Rutten | Universal coalgebra-A theory of systems[END_REF]. The datatypes are generated by their constructors, whereas the codatatypes are viewed through their selectors.

Datatypes and codatatypes share many basic properties. All properties below are implicitly universally quantified and range over all i, j, j , and k within bounds:

Distinctness: C ij ( x) ≈ C ij (ȳ) if j = j Injectivity: C ij (x 1 , . . . , x n ij ) ≈ C ij (y 1 , . . . , y n ij ) -→ x k ≈ y k Exhaustiveness: d i1 (x) ∨ • • • ∨ d im i (x) Selection: s k ij (C ij (x 1 , . . . , x n ij )) ≈ x k
Expressed in the algebraic jargon, exhaustiveness helps ensure that "no junk" exists, whereas distinctness and injectivity guarantee that "no confusion" can arise. The result of selectors applied to the wrong constructor is left completely unspecified. Datatypes are additionally characterized by an induction principle for proving a conjunction of properties P 1 , . . . , P over arbitrary values v 1 : δ 1 , . . . , v : δ : Induction:

i=1 m i j=1 ∀x 1 . . . x n ij . n ij k=1 IH [x k ] -→ P i [C ij (x 1 , . . . , x n i j )] i=1 P i [v i ]
The notation IH [x] denotes either P i [x] if there exists some i such that the formula is typecorrect or else (truth). The induction principle ensures that the interpretation of datatypes is standard. For the natural numbers constructed from Z and S, induction prohibits models that contain infinite values S(S(. . .)).

For codatatypes, the dual notion is called coinduction. It makes it possible to derive the equality of pairs of codatatype values v 1 , w 1 : δ 1 , . . . , v , w : δ , based on suitable coinduction witnesses R 1 , . . . , R :

Coinduction: i=1 R i [v i , w i ] i=1 ∀x y. R i [x, y] -→ m i j=1 d j (x) -→ d j (y) ∧ n ij k=1 s k ij (x) ∼ s k ij (y) i=1 v i ≈ w i
The notation x ∼ y stands for R i [x, y] if there exists some i such that the formula is typecorrect or x ≈ y otherwise. The second premise ensures that the coinduction witnesses are bisimulations. The first premise and the conclusion capture the notion that equality is the largest bisimulation on codatatypes. Thus, the coinduction principle encodes a form of extensionality: Two values that yield the same observations must be equal, where the observations are made through selectors and discriminators.

Example 1 The induction principle for list τ is given below: vs ≈ ws

Codatatypes are guaranteed to contain all values corresponding to infinite ground constructor terms. In general, this cannot be captured by a first-order axiomatization, since there may be uncountably many of them. For example, stream int is isomorphic to the uncountable function space nat → int. Bjørner gives a rigorous treatment of this aspect [START_REF] Bjørner | Integrating decision procedures for temporal verification[END_REF].

Given a signature Σ, DC refers to the theory of datatypes and codatatypes, which defines a class of Σ-interpretations J, namely those that satisfy the properties mentioned in this section, including (co)induction. The interpretations in J share the same interpretation for constructor terms and correctly applied selector terms (up to isomorphism) but may differ on variables and wrongly applied selector terms. A formula is DC -satisfiable if there exists an interpretation in J that satisfies it. For deciding universal formulas, induction can be replaced by the acyclicity axiom schema, which states that constructor terms cannot be equal to any of their proper subterms [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF]. Dually, coinduction can be replaced by the uniqueness schema, which asserts that codatatype values are fully characterized by their expansion [37, Theorem 8.1, 2 ⇔ 5].

For datatypes, any recursive specification gives rise to an infinite datatype. Paradoxically, this does not extend to codatatypes: Some codatatypes are so degenerate as to be finite even though they have infinite values. A simple example is codatatype a = A(a), which is corecursive and yet has a cardinality of one; its unique value is µa. A(a). Other specimens are stream unit and both b and c in the specification

codatatype b = B(b, c, b, unit) and c = C(a, b, c)
assuming unit is a datatype with the single constructor Unity : unit. We call such codatatypes corecursive singletons, or simply singletons. For the decision procedure, it will be crucial to detect these. A type may also be a corecursive singleton only in some models. If the example above is altered to make unit an uninterpreted type, b and c will be singletons precisely when unit is interpreted as a singleton. Fortunately, given cardinalities for the ordinary types, it is easy to characterize this degenerate case.

Lemma 1 Let δ be a corecursive codatatype. For any interpretation in J, the domain interpreting δ is either infinite or a singleton. In the latter case, δ necessarily has a single constructor, whose arguments have types that are interpreted as singleton domains.

Proof By definition, the type is equipped with at least one (directly or indirectly) corecursive constructor C. If it additional has second corecursive constructor D, it is possible to encode infinitely many alternation patterns-e.g., C(D(C(C(. . .))))-all of which correspond to distinct values (by distinctness and injectivity). If the type has a noncorecursive constructor E, it is possible to create terms of arbitrary depth-e.g., C(. . . (C(E)) . . .). In either case, there can be no finite models. Therefore, C must be the only constructor. If any of its noncorecursive arguments has a cardinality greater than 1, it is possible to encode alternation patterns using it-e.g., C(0, C(1, C(0, C(0, . . .))))-which again excludes finite models. Otherwise, the coinduction principle ensures that the type has at most one value.

The Decision Procedure

Given a fixed signature Σ, the decision procedure for the universal theory of (co)datatypes determines the DC -satisfiability of finite sets E of literals: equalities and disequalities be-tween Σ-terms, whose variables are interpreted existentially. The decision procedure is formulated as a tableau-like calculus. Proving a universal quantifier-free conjecture is reduced to showing that its negation is unsatisfiable. The presentation is inspired by Barrett et al. [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF] but at a higher level, using unoriented equations instead of oriented ones.

To simplify the presentation, we make a few assumptions about Σ. First, all codatatypes are corecursive. This is reasonable because noncorecursive codatatypes can be seen as nonrecursive datatypes. Second, all ordinary types have infinite cardinality. Without quantifiers, the constraints E cannot entail an upper bound on the cardinality of any uninterpreted type, so it is safe to consider these types infinite. As for ordinary types interpreted finitely by other theories (e.g., bit vectors), each interpreted type having finite cardinality n can be viewed as a datatype with n nullary constructors [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF].

A Calculus for DC

Our calculus for DC consists of derivation rules. A derivation rule can be applied to E if its premises are met. The conclusion either specifies equalities to be added to E or is ⊥ (contradiction). One of the rules has multiple conclusions, denoting branching. An application of a rule is redundant if one of its non-⊥ conclusions leaves E unchanged. A derivation tree is a tree whose nodes are finite sets of equalities, such that child nodes are obtained by a nonredundant application of a derivation rule to the parent. A derivation tree is closed if all of its leaf nodes are ⊥. A node is saturated if no nonredundant instance of a rule can be applied to it.

The derivation rules are partitioned into three sets of rules, given in Figs. 1 to 3, corresponding to three phases of the calculus. The first phase computes the bidirectional closure of E. The second phase makes inferences based on acyclicity (for datatypes) and uniqueness (for codatatypes). The third phase performs case distinctions on constructors for various terms occurring in E. The rules belonging to a phase have priority over those of subsequent phases. The rules are applied until the derivation tree is closed or all leaf nodes are saturated.

Phase 1: Computing the Bidirectional Closure (Fig. 1). In conjunction with Refl, Sym, and Trans, the Cong rule computes the congruence (upward) closure, whereas the Inject and Clash rules compute the unification (downward) closure. For unification, equalities are inferred based on the injectivity of constructors by Inject, and failures to unify equated terms are recognized by Clash. The Conflict rule recognizes when an equality and its negation both occur in E, in which case E has no model. Let T (E) denote the set of Σ-terms occurring in E. At the end of the first phase, E induces an equivalence relation over T (E) such that two terms t and u are equivalent if and only if t ≈ u ∈ E. Thus, we can regard E as a set of equivalence classes of terms. For a term t ∈ T (E), we write [t] to denote the equivalence class of t in E. Moreover, at the end of this phase, each equivalence class [t] contains at most one constructor term that is unique up to congruence. Thus, in the subsequent phases, when considering the case that [t] contains constructor terms, it is enough to select an arbitrary constructor term C(t ) ∈ [t] among these.

Phase 2: Applying Acyclicity and Uniqueness (Fig. 2). The rules in this phase are described in terms of a mapping A that assigns to each equivalence class a µ-term as its representative.

Formally, µ-terms are defined recursively as being either a variable x or an applied constructor µx. C(t ) for some C ∈ F ctr and µ-terms t of the expected types. The variable x need

t ∈ T (E) t ≈ t ∈ E Refl t ≈ u ∈ E u ≈ t ∈ E Sym s ≈ t, t ≈ u ∈ E s ≈ u ∈ E Trans t ≈ ū ∈ E f(t ), f( ū) ∈ T (E) f(t ) ≈ f( ū) ∈ E Cong t ≈ u, t ≈ u ∈ E ⊥ Conflict C(t ) ≈ C( ū) ∈ E t ≈ ū ∈ E Inject C(t ) ≈ D( ū) ∈ E C = D ⊥ Clash Fig. 1 Derivation rules for bidirectional closure δ ∈ Y dt A [t δ ] = µx. u x ∈ FV(u) ⊥ Acyclic δ ∈ Y codt A [t δ ] = α A [u δ ] t ≈ u ∈ E Unique Fig. 2
Derivation rules for acyclicity and uniqueness

t δ ∈ T (E) F δ ctr = {C 1 , . . . , C m } s(t) ∈ T (E) and s ∈ F δ sel or δ ∈ Y dt and δ is finite t ≈ C 1 s 1 1 (t), . . . , s n 1 1 (t) ∈ E • • • t ≈ C m s 1 m (t), . . . , s n m m (t) ∈ E Split t δ , u δ ∈ T (E) δ ∈ Y codt δ is a singleton t ≈ u ∈ E Single Fig. 3
u ∈ FV(A ) C(t 1 , . . . , t n ) ∈ [u] C ∈ F ctr A := A [ u → µ u. C( t 1 , . . . , t n )] FV(A )
A = {[x] → µ x. C( w, y)} 2. Unfold y: A = {[x] → µ x. C( w, µ y. C( z, x)), [y] → µ y. C( z, x)} 3. Unfold x: A = {[x] → µ x. C( w, µ y. C( z, x)), [y] → µ y. C( z, µ x. C( w, y))}
The resulting A indicates that the values for x and y in models of E must be of the forms

A [t], A [u] are α-equivalent, then t ≈ u.
Comparison for α-equivalence may seem too restrictive, since µx. S(x) and µy. S(S(y)) specify the same value despite being α-disequivalent, but the rule will make progress by discovering that the subterm S(y) of µy. S(S(y)) must be equal to the entire term, as demonstrated next. Since A [y] = α A [S(y)], the Unique rule applies to derive y ≈ S(y). At this point, phase 1 is activated again, yielding the equivalence classes {x, S(x)} and {y, S(y), S(S(y))}. The mapping A is updated accordingly:

A [x] = µ x. S( x) A [y] = µ y. S( y) Since A [x] = α A [y],
Unique can finally be applied to derive x ≈ y.

Phase 3: Branching (Fig. 3). If a selector is applied to a term t, or if t's type is a finite datatype, t's equivalence class must contain a δ constructor term. This is enforced in the third phase by the Split rule. Another rule, Single, focuses on the degenerate case where two terms have the same corecursive singleton type and are therefore equal. Both Split's finiteness assumption and Single's singleton constraint can be evaluated statically based on a recursive computation of the cardinalities of the constructors' argument types.

Termination and Correctness of the Calculus

We now show the termination and correctness of the calculus. Correctness means the following: If there exists a closed derivation tree with root node E, then E is DC -unsatisfiable;

and if there exists a derivation tree with root node E that contains a saturated node, then E is DC -satisfiable.

Theorem 1 (Termination) All derivation trees are finite.

Proof Consider a derivation tree with root node E. Let D ⊆ T (E) be the set of terms whose types are finite datatypes, and let S ⊆ T (E) be the set of terms occurring as arguments to selectors. For each term t ∈ D, let

S 0 t = {t} S i+1 t = S i t ∪ {s(u) | u δ ∈ S i t , δ ∈ Y dt , |δ| is finite, s ∈ F δ sel }
and let S ∞ t be the limit of this sequence. This is a finite set for each t, because all chains of selectors applied to t are finite. Let S ∞ be the union of all sets S ∞ t where t ∈ D, and let T ∞ (E) be the set of subterms of E ∪ {C j s 1 j (t), . . . ,

s n j j (t) | t δ ∈ S ∪ S ∞ , C j ∈ F δ ctr }.
In a derivation tree with root node E, it can be shown by induction on the rules of the calculus that each nonroot node F is such that T (F) ⊆ T ∞ (E), and hence contains an equality between two terms from T ∞ (E) not occurring in its parent node. Thus, the depth of a branch in a derivation tree with root node E is at most

|T ∞ (E)| 2 , which is finite since T ∞ (E) is finite.
Theorem 2 (Refutation Soundness) If there exists a closed derivation tree with root node E, then E is DC -unsatisfiable.

Proof The proof is by structural induction on the derivation tree with root node E. If the tree is an application of Conflict, Clash, or Acyclic, then E is DC -unsatisfiable. For Conflict, this is a consequence of equality reasoning. For Clash, this is a consequence of distinctness. For It remains to show the converse of the previous theorem: If a derivation tree with root node E contains a saturated node, then E is DC -satisfiable. The proof relies on a specific interpretation J that satisfies E. First, we define the set of interpretations of the theory DC , which requires custom terminology concerning µ-terms. Given a µ-term t with subterm u, the expansion of u with respect to t is the µ-term u / 0 t , abbreviated to u t , as returned by the function

x B t = x if x ∈ B µx. C ū B {x} t if µx. C( ū) binds this occurrence of x / ∈ B in t µx. C( ū) B t = x if x ∈ B µx. C ū B {x} t otherwise
The recursion will eventually terminate because each recursive call adds one bound variable to B and there are finitely many distinct bound variables in a µ-term. Intuitively, the expansion of a subterm is a self-contained µ-term that denotes the same value as the original subterm-e.g., µy. D(x) µ x. C(µy. D(x)) = µy. D(µ x. C(y)).

The µ-term u is a self-similar subterm of t if u is a proper subterm of t, t and u are of the forms µx. C(t 1 , . . . , t n ) and µy. C(u 1 , . . . , u n ), and t k t = α u k t for all k. The µ-term t is normal if it does not contain self-similar subterms and all of its proper subterms are also normal. Thus, t = µx. C(µy. C(y)) is not normal because µy. C(y) is a self-similar subterm of t. Their arguments have the same expansion with respect to t: µy. C(y) t = µy. C y {y} For any µ-term t of the form µx. C( ū), its normal form t is obtained by replacing all of the self-similar subterms of t with x and by recursively normalizing the other subterms. For variables, x = x. Thus, µx. C(µy. C(x)) = µx. C(x).

We now define the class of interpretations for DC . J (τ) denotes the interpretation type τ in J -that is, a nonempty set of domain elements for that type. J (f) denotes the interpretation of a function f in J .

If f : τ 1 × • • • × τ n → τ, then J (f) is a total function from J (τ 1 ) × • • • × J (τ n ) to J (τ).
All types are interpreted as sets of µ-terms, but only values of types in Y codt may contain cycles.

Definition 1 (Normal Interpretation) An interpretation J is normal if the following conditions are met:

1. For each type τ, J (τ) includes a maximal set of closed normal µ-terms of that type that are unique up to α-equivalence and acyclic unless τ ∈ Y codt . 2. For each constructor term C(t ) of type τ, J (C)(J (t )) is the value in J (τ) that is αequivalent to µx. C(J (t )) , where x is fresh.

For each selector term s

k j (t) of type τ, if J (t) is µx. C j (ū), then J (s k j ) J (t) is the value in J (τ) that is α-equivalent to u k J (t) .
Not all normal interpretations are models of codatatypes, because models must contain all possible infinite terms, not only cyclic ones. However, acyclic infinite values are not interesting for deciding universal formulas: For such formulas, it is trivial to extend any normal interpretation with extra domain elements to obtain a genuine model if desired.

When constructing a model J of E, it remains only to specify how J interprets wrongly applied selector terms and variables. For the latter, this will be based on the mapping A computed in phase 2 of the calculus.

First, we need the following definitions. We write t = x α u if µ-terms t and u are syntactically equivalent for some renaming that avoids capturing any variable other than x. For example, µx. D(x) = y α µx. D(y) (by renaming y to x), µx. C(x, x) = x α µy. C(x, y), and µx. C(z, x) = z α µy. C(z, y), but µx. D(x) = x α µx. D(y) and µx. C(x, x) = y α µy. C(x, y). For a variable x τ and a normal interpretation J , we let V x J (A ) denote the set consisting of all values v ∈ J (τ) such that v = x α u t for some subterm u of a term t occurring in the range of A .

This set describes shapes of terms to avoid when assigning a µ-term to x.

The completion A of A for a normal interpretation J assigns values from J to unassigned variables in the domain of A . We construct A by initially setting A := A and by exhaustively applying the following rule:

x τ ∈ FV(A ) µ x. t = α v v ∈ J (τ) v / ∈ V x J (A ) A := A [ x → µ x. t]
Given an unassigned variable in A , this rule assigns it a fresh value-one that does not occur in V x J (A ) modulo α-equivalence-excluding not only existing terms in the range of A but also terms that could emerge as a result of the update. Since this update removes one variable from FV(A ) and does not add any variables to FV(A ), the process eventually terminates. We normalize all terms in the range of A at each step.

To ensure disequality literals are satisfied by an interpretation based on A , it suffices that A is injective modulo α-equivalence. This invariant holds initially, and the last premise in the above rule ensures that it is maintained. The set V x J (A ) is an overapproximation of the values that, when assigned to x, will cause values in the range of A to become α-equivalent. For infinite codatatypes, it is always possible to find fresh values v because

V x J (A ) is a finite set.
Example 4 Let δ be a codatatype with the constructors C, D, E : δ → δ. Let E be the set {u ≈ C(z), v ≈ D(z), w ≈ E(y), x ≈ C(v), v ≈ s, z ≈ v}. After applying the calculus to saturation on E, the mapping A is as follows:

A [u] = µ u. C( z) A [w] = µ w. E( y) A [y] = y A [v] = µ v. D( z) A [x] = µ x. C(µ v. D( z)) A [z] = z
Here

J (u) = A [u], J (v) = A [v],
and so on. Assigning a value for A [z] that is α-equivalent to a value in V z J (A ) may cause values in the range of A to become α-equivalent, which in turn may cause E to be falsified by J . For example, assign µ z. D( z) for z. After the substitution,

A [v] = µ v. D(µ z. D( z)),
which has normal form µ v. D( v), which is α-equivalent to µ z. D( z). However, this contradicts the disequality z ≈ v in E. On the other hand, if the value assigned to z is fresh, the values in the range of A remain α-disequivalent. We can assign a value such as µ z. E( z),

µ z. D(C( z)), or µ z. C(C(D( z))) to z.
Legal substitutions for z may cause the range of A to contain abnormal terms. For example, after assigning µ z. D(C( z)) to z, we have

A [u] = µ u. C(µ z. D(C( z))), with normal form µ u. C(µ z. D( u)
). This explains why the term is normalized in the rule's conclusion.

In the following lemma about A , Var(t) = t if t is a variable

x if t is of the form µx. u.
Lemma 2 If A is constructed for a saturated set E and A is a completion of A for a normal interpretation J , the following properties hold for all [x] and [y] in the domain of A :

(1) A [x τ ] is α-equivalent to a value in J (τ). (2) A [x] = t A [y] for all subterms t of A [y] with Var(t) = x. (3) A [x] = α A [y] if and only if [x] = [y].
Proof To show (1), we first show that A contains no free variables. Assume by contradiction that A contains a free variable y for some [y] of type τ. Then it must be the case that [y] does not contain a constructor term, or else y would not occur as a free variable in A .

Consider the case when τ is finite. By assumption, τ / ∈ Y ord . Since Split does not apply to

E, we have τ / ∈ Y dt . If τ ∈ Y codt ,
then τ is corecursive by assumption, and by Lemma 1, the cardinality of τ must be one. Since Single does not apply, there is only one equivalence class of type τ in E, and thus there are no terms in V y J (A ) of type τ. This is a contradiction, since completion can assign the value in the domain of τ to y. Now, consider the case when τ is infinite. This is also a contradiction, since there are only a finite number of closed terms in V y J (A ), and thus completion can assign a value not occurring in V y J (A ) to y. By construction, A [x] is normal. Since Acyclic does not apply, A [x] is acyclic when τ ∈ Y dt . Moreover, the construction of A applies substitutions of the form { y → t}, where t is acyclic when the type of y is not a codatatype. Thus, A [x] is acyclic when τ / ∈ Y codt . Therefore, by definition, A [x] is α-equivalent to a value in J (τ).

We now show that ( 2) and ( 3 constructed by a sequence of substitutions of the form mentioned above to z. Thus, we have

t A [y] = A [x] A [x] = A [x]
, and (2) holds for A . Property (3) holds for A since Unique does not apply.

We now show that A = A . Assume by contradiction A

[x] = A [x] for some A [x] of minimal size. We have that A [x] is of the form µ x. C(t 1 , . . . , t n ). Due to the construction of A , we know [x] contains a constructor C(z 1 , . . . , z n ) and Var(t i ) = z i for some i. Since A [x]
is a minimal, it contains a subterm of the form µ y. C(u 1 , . . . , u n ) where

t i A [x] = α u i A [x]
for some i. Due to the construction of A , [y] contains a constructor C(w 1 , . . . , w n ) and Var(u i ) = w i for some i. Since Cong does not apply, we have [w j ] and [z j ] are distinct for some j. By (2),

t j A [x] = A [z j ] and u j A [x] = A [w j ], which are not α-equivalent by (3), contradicting the fact that µ y. C(u 1 , . . . , u n ) is a self-similar subterm of A [x]
. Thus, A = A , and ( 2) and ( 3) hold for A .

We now show that if ( 2) and ( 3) hold for some A 1 , they also hold for A 1 σ , where σ is a substitution of the form { x → µ x. t}, x ∈ FV(A 1 ), and µ x. t is not α-equivalent to a term in

V x J (A 1 ). To show (2), by assumption of (2) on A 1 , we have u A 1 [y] = A 1 [x] for all subterms u of A 1 [y] where Var(t) = x. Thus, u A 1 σ[y] = A 1 σ[x] and u A 1 σ [y] = A 1 σ [x].
t 1 = α t 2 . If t 1 (resp. t 2 ) is a free variable that is not x, then A 1 σ [y] (resp. A 1 σ [z]) contains t 1 (resp. t 2 )
at position p, and A 1 σ [z] (resp. A 1 σ [y]) does not. If t 1 is of the form µw 1 . C(t ) and t 2 is of the form µw 2 . D( ū), then the expansion of A 1 σ [y] and A 1 σ [z] are α-disequivalent at position p.

Since t 1 and t 2 are minimal, say t 1 is of the form µw. C(t ), and t 2 is x. Since σ maps x to a closed µ-term µ x. t, we have that FV(t 1 ) ⊆ { x}, or else the expansion of A 1 σ [y] and A 1 σ [z] are α-disequivalent at position p since they do not contain the same free variables. Since

t 1 A 1 [y] is normal, there is a closed µ-term v ∈ V x J (A 1 ) such that v = x α t 1 A 1 [y]
. Thus, by assumption on the selection of µ x. t, we have µ

x. t = x α t 1 A 1 [y]
, which implies that the expansion of A 1 σ [y] and A 1 σ [z] are α-disequivalent at position p. Thus, by induction on the number of applications of the above rule used to obtain A , we have that A satisfies (2) and (3).

Intuitively, this lemma states three properties of A that together ensure that a normal interpretation J can be constructed that satisfies E. Property (1) states that the values in the range of A are α-equivalent to a value in normal interpretation. This means they are closed, normal, and acyclic when required. Property [START_REF] Barrett | The SMT-LIB standard: Version 2.5[END_REF] states that the interpretation of all subterms in the range of A depends on its associated variable only. In other words, the interpretation of a subterm t where Var(t) = x is equal to A [x], independently of the context. Property (3) states that A is injective (modulo α-equivalence), which ensures that distinct values are assigned to distinct equivalence classes.

Example 5 Consider A from Example 4. While extending A to its corresponding completion A , we may, for instance, assign µ z. E( z) to z, and subsequently assign µ y. D( y) to y. We obtain the following mapping A from equivalence classes to µ-terms:

A [u] = µ u. C(µ z. E( z)) A [w] = µ w. E(µ y. D( y)) A [y] = µ y. D( y) A [v] = µ v. D(µ z. E( z)) A [x] = µ x. C(µ v. D(µ z. E( z))) A [z] = µ z. E( z)
Notice that A satisfies the properties from Lemma 2 for a normal interpretation J : All terms in the range of A are closed and normal, A [s] = t A [y] for all subterms t where Var(t) = s for all s, and all terms in the range of A are pairwise α-disequivalent. We may construct an interpretation J where variables are interpreted as the value that is α-equivalent to one from J (δ) and that is uniquely associated with its equivalence class by A .

Theorem 3 (Solution Soundness) If there exists a derivation tree with root node E containing a saturated node, then E is DC -satisfiable.

Proof Let F be a saturated node in a derivation tree with root node E. We consider a normal interpretation J that interprets wrongly applied selectors based on equality information in F and that interprets the variables of F based on the completion A . For the variables, let J (x τ ) be the value in J (τ) that is α-equivalent with A [x] for each variable x ∈ T (F), which by Lemma 2(1) is guaranteed to exist.

We first show that J satisfies all equalities t 1 ≈ t 2 ∈ F. To achieve this, we show by structural induction on t τ that J

(t) = α A [t] for all terms t ∈ T (F), which implies J t 1 ≈ t 2 since J is normal. If t is a variable, then J (t) = α A [t] by construction.
If t is a constructor term of the form C(u 1 , . . . , u n ), then J (t) is α-equivalent with µx. C(J (u 1 ), . . . , J (u n )) for some fresh x, which by the induction hypothesis is α-equivalent with µx. C(A [u 1 ], . . . , A [u n ]) . Call this term t . Since Inject and Clash do not apply to F, by the construction of A we have that A [t] is a term of the form µ t. C(w 1 , . . . , w n ) where Var(w i ) = u i for each i. Thus by Lemma 2(2), w i A [t] = A [u i ]. For each i, let u i be the ith argument of t . We have that u i t = α A [u i ], and thus u i t = α w i A [t] . Thus,

J (t) = α t = α A [t]
, and we have

J (t) = α A [t].
If t is a selector term s k j (u), since Split does not apply to F, [u] must contain a term of the form C j s 1 j (u), . . . , s n j (u) for some j . Since Inject and Clash are not applicable, by construction A [u] must be of the form µ u. C j (w 1 , . . . , w n ), where Var(w i ) = s i j (u) for each i, and thus by Lemma 2(2),

w i A [u] = A [s i j (u)]. If j = j , then J (t) is α-equivalent with w k A [u] , which is equal to A [s k j (u)] = A [t]
. If j = j , since Cong does not apply, any term of the form s k j (u ) not occurring in [t] is such that [u] = [u ]. By the induction hypothesis and Lemma 2(3), J (u) = J (u ) for all such u, u . Thus, we may interpret J (s k j )(J (u)) as the value in J (τ) that is α-equivalent with A [t].

We now show that all disequalities in F are satisfied by J . Assume t ≈ u ∈ F. Since Example 6 Continuing Example 5, let J be a normal interpretation, where up to renaming of µ-bound variables, we have

J (u) = C(µ z. E( z)) J (w) = E(µ y. D( y)) J (y) = µ y. D( y) J (s) = J (v) = D(µ z. E( z)) J (x) = C(D(µ z. E( z))) J (z) = µ z. E( z)
It is easy to see that J satisfies the constraints

u ≈ C(z) v ≈ D(z) w ≈ E(y) x ≈ C(v) v ≈ s z ≈ v
By Theorems 1, 2, and 3, the calculus is sound and complete for the universal theory of (co)datatypes. We may rightly call it a decision procedure for that theory. The proof of solution soundness is constructive in that it provides a method for constructing a model for a saturated configuration, by means of the mapping A .

Implementation in CVC4

The decision procedure was presented at a high level of abstraction, omitting quite a few details. This section describes the main aspects of the implementation within the SMT solver CVC4: the integration of the procedure into CDCL(T ) [START_REF] Ganzinger | DPLL(T ): Fast decision procedures[END_REF], the construction of models with µ-terms, and the extension of the procedure to quantified formulas.

A Theory Solver for DC

The decision procedure is implemented as a theory solver of CVC4-that is, a specialized procedure for determining the satisfiability of conjunctions of literals for its theory. Given a theory T = T 1 ∪ • • • ∪ T n and a set of input clauses F in conjunctive normal form, the CDCL(T ) procedure incrementally builds partial assignments of truth values to the atoms of F such that no clause in F is falsified. We can regard such a partial assignment as a set M of true literals. By a variant [START_REF] Jovanović | Sharing is caring: Combination of theories[END_REF] of the Nelson-Oppen method [START_REF] Nelson | Simplification by cooperating decision procedures[END_REF], each T i -solver takes as input the union M i of the purified form of T i -literals occurring in M, where fresh variables replace terms containing symbols not belonging to T i ; additional (dis)equalities between variables of types not belonging to T i .

Each T i -solver either reports that a subset C of M i is T i -unsatisfiable, in which case ¬ C is added to F, adds a clause to F, or does nothing. When M is a complete assignment for F, a theory solver can choose to do nothing only if M i is indeed T i -satisfiable.

Assume E is initially the set M i described above. With each equality t ≈ u added to E, we associate a set of equalities from M i that together entail t ≈ u, which we call its explanation. Similarly, each A [x] is assigned an explanation-that is, a set of equalities from M i that entail that the values of [x] in models of E are of the form A

[x]. For example, if x ≈ C(x) ∈ M i , then x ≈ C(x) is an explanation for A [x] = µ x. C( x).
If multiple rules can derive the same conclusion, the solver simply keeps the first explanation it encounters.

The rules of the calculus are implemented as follows. For all rules with conclusion ⊥, we report the union of the explanations for all premises is DC -unsatisfiable. The implementation does not use any techniques to minimize the size of this set, which in some cases may be non-minimal. For Split, we add the exhaustiveness clause m (t) to F. Decisions on which branch to take are thus performed externally by the SAT solver. All other rules add equalities to the internal state of the theory solver. The rules in phase 1 are performed eagerly-that is, for partial satisfying assignments M-while the rules in phases 2 and 3 are performed only for complete satisfying assignments M.

U := U ∪ U i . 2.3. U := U . 3. If distinct [t], [u] ∈ U for some U ∈ U, Unique(t, u).
Before constructing a model for F, the theory solver constructs neither µ-terms nor the mapping A . Instead, it relies on the algorithms in Figs. 4 and5 for determining whether the rules Acyclic and Unique apply to the set E. For Acyclic, Fig. 4 considers the set U of all datatype equivalence classes of E. We choose an arbitrary [t] in U and call the recursive subprocedure Traverse, which takes as input the current equivalence class we are processing, the set of equivalence classes U we have yet to process, and the set of equivalence classes P we are currently processing. If a call to For Unique, Fig. 5 considers a partition U of the equivalence classes of our set E such that codatatype equivalence classes having a constructor term with top symbol C are placed in the same subset, for each constructor C. We write [t] = U [u] to denote that [t] and [u] reside in the same subset within U. We then refine U by constructing a partition U i of each U i ∈ U such that distinct [t] and [u] reside in the same subset of U i if and only if they contain constructor terms C(t 1 , . . . , t k ) and C(u 1 , . . . , u k ) where each t j , u j are such that [t j ] and [u j ] reside in the same subset of U for each j = 1, . . . , k. Let U be the union of each of these partitions. We update U to U . This refinement is repeated until U is left unchanged. If the resulting partition U contains a subset U having two distinct equivalence classes [t] and [u], then Unique applies to t and u. This algorithm is analogous to Hopcroft's algorithm for minimizing deterministic finite automata [START_REF] Hopcroft | An n log n algorithm for minimizing states in a finite automaton[END_REF]-terms correspond to states, argument positions 1, . . . , k correspond to input symbols, and the top constructor symbol of a term generalizes the accepting/rejecting status of a state.

The implementation of the decision procedure uses several optimizations following the lines of Barrett et al. [START_REF] Barrett | An abstract decision procedure for satisfiability in the theory of inductive data types[END_REF]. We briefly mention the main ones. Discriminators are part of the signature and not abbreviations. This requires extending the decision procedure with several rules, which apply uniformly to datatypes and codatatypes. This approach often leads to better performance because it introduces terms less eagerly to T (E). Selectors are collapsed eagerly: If s k j (t) ∈ T (E) and t = C j (u 1 , . . . , u n ), the solver directly adds s k j (t) ≈ u k to E, whereas the presented calculus would apply Split and Inject before adding this equality. To reduce the number of unique literals considered by the calculus, we compute a normal form for literals as a preprocessing step. In particular, we replace u ≈ t by t ≈ u if t is smaller than u with respect to some term ordering, replace C j (t ) ≈ C j (ū) with ⊥ when j = j , replace all selector terms of the form s k j (C j (t 1 , . . . , t n )) by t k , and replace occurrences of discriminators d j (C j (t )) by or ⊥ based on whether j = j . Finally, finite ordinary types are not converted to finite datatypes. We instead rely on standard extensions of the Nelson-Oppen method [START_REF] Tinelli | Combining nonstably infinite theories[END_REF], which impose requirements regarding terms having finite sorts are shared between multiple theories. In particular, given an ordinary type τ of finite cardinality n belonging to theory T i , the theory solver for T i must communicate enough equalities over shared terms to ensure that all other theory solvers, including the one for DC , interpret τ as a set having cardinality at most n.

As Barrett et al. observed for their procedure, it is both theoretically and empirically beneficial to delay applications of Split as long as possible. Similarly, Acyclic and Unique are fairly expensive because they require traversing the equivalence classes, which is why they are part of phase 2.

Model Construction

When instructed to do so, the implementation produces models for satisfiable inputs. As described in Section 3.2, given a saturated set E, we construct a map A from the equivalence classes of E to closed normal µ-terms. Recall that our construction of A requires choosing values µ x. t for each x ∈ FV(A ) such that µ x. t does not occur in the set V x J (A ). To choose values, we use a fair enumerator for each (co)datatype τ, which lists all the values of type τ in a normal interpretation.

For codatatypes, we enumerate a stream of every µ-term of our signature Σ in a fair manner, discarding those that have free variables or are not normal. For those that are closed and normal, we then check whether they occur in the set V x J (A ). This set does not need to be explicitly constructed. To determine if a term µ x. t occurs in the set V x J (A ), we check if it is α-equivalent to a closed term (µ y. u){ x → z} for some µ y. u in the range of A and variable z. This can be efficiently achieved by matching the term µ x. t with µ y. u.

Extension to Quantified Formulas

While the decision procedure is restricted to universal conjectures, users often want to solve problems that feature universal axioms and existential conjectures. Many SMT solvers, including CVC4, can reason about quantified formulas using incomplete instantiation-based techniques [START_REF] De Moura | Efficient E-matching for SMT solvers[END_REF][START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF]. These techniques extend naturally to quantified formulas involving datatypes and codatatypes.

However, the presence of quantifiers poses an additional challenge in the context of (co)datatypes. Quantified formulas can entail an upper bound on the cardinality of an uninterpreted type u. Since it assumes that uninterpreted types have infinite cardinality, the calculus presented in Section 3 is incomplete since it may fail to recognize cases where Split and Single should be applied. This does not impact the correctness of the procedure in this setting, since the solver is already incomplete for quantified formulas.

Nonetheless, two techniques help increase the precision of the solver. First, we can apply Split to datatype terms whose cardinality depends on the finiteness of uninterpreted types. Second, we can conditionally apply Single to codatatype terms whose type potentially has cardinality one. For example, the codatatype stream u has cardinality one precisely when u has cardinality one. If there exist two equivalence classes [s] and [t] for this type, the implementation adds the clause (∃x y u . x ≈ y) ∨ s ≈ t to F, which states that either the cardinality of u is greater than one or s must be equal to t.

Evaluation on Isabelle Problems

The decision procedure for (co)datatypes is useful both for proving (via negation, in the refutational style) and for model finding [START_REF] Ge | Complete instantiation for quantified formulas in satisfiability modulo theories[END_REF][START_REF] Reynolds | Quantifier instantiation techniques for finite model finding in SMT[END_REF]. It is in fact vital for finite model finding, because the acyclicity and uniqueness rules are necessary for solution soundness, without which the generated models would often be spurious. For example, given the constraints zeros ≈ SCons(0, zeros) repeat(n) ≈ SCons(n, repeat(n))

on streams, the conjecture zeros ≈ repeat(0) would be "refuted" by a spurious countermodel that interprets zero and repeat(0) by two distinct values that both correspond to the term µs. SCons(0, s), violating uniqueness. By contrast, the contributions of the decision procedure to proving are less obvious; they depend on how often acyclicity and uniqueness are necessary for a proof. To evaluate this, we generated benchmark problems from existing interactive proof goals arising in existing Isabelle formalizations, using Sledgehammer [START_REF] Blanchette | Extending Sledgehammer with SMT solvers[END_REF] as translator from Isabelle to SMT-LIB. We included all the formalizations from the Isabelle distribution (Distro, 1179 goals) and the Archive of Formal Proofs (AFP, 3014 goals) [START_REF]Archive of Formal Proofs[END_REF] that define codatatypes falling within the supported fragment. We also included formalizations about Bird and Stern-Brocot trees (SBT, 265 goals) [START_REF] Gammie | The Stern-Brocot tree[END_REF]. To exercise the datatype support, formalizations about finite lists and trees were added to the first two benchmark sets. The formalizations were selected before conducting any experiments. The experimental data are available online. 3For each proof goal in each formalization, we used Sledgehammer to select either 16 or 256 lemmas, which were monomorphized and translated to SMT-LIB along with the goal. The resulting problem was given to the development version of CVC4 (from 15 September lemma num_mod_den_unique: x = Node 0 num x =⇒ x = num_mod_den proof (coinduction arbitrary: x rule: tree.coinduct_strong) case (Eq_tree x) show ?case by (subst (1 2 3 4) Eq_tree) (simp add: eqTrueI[OF Eq_tree]) qed

The tree num_mod_den is defined as num_mod_den = Node 0 num num_mod_den.

Conclusion

We introduced a decision procedure for the universal theory of datatypes and codatatypes. Our main contribution has been the support for codatatypes. Both the metatheory and the implementation in CVC4 rely on µ-terms to represent cyclic values. Although this aspect is primarily motivated by codatatypes, it makes a uniform account of datatypes and codatatypes possible-in particular, the acyclicity rule for datatypes exploits µ-terms to detect cycles. The empirical results on Isabelle benchmarks confirm that CVC4's new capabilities improve the state of the art.

This work is part of a wider program that aims at enriching automatic provers with high-level features and at reducing the gap between automatic and interactive theorem proving. We are currently interfacing CVC4's finite model finding capabilities for generating counterexamples in proof assistants [START_REF] Reynolds | Model finding for recursive functions in SMT[END_REF]; in this context, the acyclicity and uniqueness rules are crucial to exclude spurious countermodels. As future work, it would be useful to implement proof reconstruction for (co)datatype inferences in Isabelle. In addition, it might be worthwhile to extend SMT solvers with dedicated support for (co)recursion.

Example 3

 3 Let E = {x ≈ S(x), y ≈ S(S(y))}. After phase 1, the equivalence classes are {x, S(x)}, {y, S(S(y))}, and {S(y)}. Constructing A yields A [x] = µ x. S( x) A [y] = µ y. S(µ S(y). S( y)) A [S(y)] = µ S(y). S(µ y. S( S(y)))

t =

 t µy. C(y) is α-equivalent to y t = µy. C y {y} t = µy. C(y). The term u = µx. C(µy. C(x)) is also not normal, since µy. C(x) is a self-similar subterm of u, noting that µy. C(x) u = µy. C x {y} u = µy. C µx. C(µy. C(x)) {y} u = µy. C µx. C( µy. C(x) {x,y} u ) = µy. C(µ x. C(y)) is α-equivalent to x u = u.

  , [u] denotes the equivalence class {u, C(z)}, [v] denotes {v, C(z), s}, and so on. To construct a completion A , we must choose values for y and z, which are free in A . Modulo α-equivalence, V z J (A ) = {µa. C(a), µa. D(a), µa. C(D(a)), C(µa. D(a))}. Now consider a normal interpretation J that evaluates variables in E based on A :

  To show (3), consider two distinct equivalence classes [y] and [z], and assume by contradiction that A 1 σ [y] = α A 1 σ [z]. Due to (3) for A 1 , [y] and [z] must have (minimal) subterms where t 1 occurs in A 1 [y] the same position p as t 2 occurs in A 1 [z], and

Fig. 5

 5 Fig. 5 Algorithm for applying the Unique rule

  Defaults are assumed for the selector names if they are omitted. The δ constructors and selectors are denoted by F δ ctr and F δ sel . For types with several constructors, it is useful to provide discriminators d ij : δ i → bool. Instead of extending F , we let d ij (t) be an abbreviation for t ≈ C ij s 1 ij (t), . . . , s n ij ij (t) . Here are a few examples of legal specifications of (co)datatype families: datatype list τ = Nil | Cons(hd: τ, tl: list τ ) codatatype llist τ = LNil | LCons(lhd: τ, ltl: llist τ ) datatype tree τ = Node(τ, forest τ ) and forest τ = FNil | FCons(tree τ , forest τ )

  Assuming that lnull and its negation are the discriminators associated with LNil and LCons, the coinduction principle for llist τ is

		P[Nil] ∀x, xs. P[xs] -→ P[Cons(x, xs)]
		P[vs]
		∀xs ys. R[xs, ys] -→ lnull(xs) -→ lnull(ys)
	R[vs, ws]	∧ ¬ lnull(xs) -→ ¬ lnull(ys) ∧ hd(xs) ≈ hd(ys) ∧ R[tl(xs), tl(ys)]

  For a term t ∈ T (E), we write t to denote the variable associated with the equivalence class [t]. Initially, we set A [u] := u for each equivalence class [u]. Because u is unconstrained, this indicates that there are initially no constraints on the values for any equivalence class [u]. The mapping A is refined by applying the following unfolding rule exhaustively:

Derivation rules for branching not occur free in the µ-binder's body, in which case the binder can be omitted. FV(t) denotes the set of free variables occurring in the µ-term t. A µ-term is closed if it contains no free variables. It is cyclic if it contains a bound variable. The α-equivalence relation t = α u indicates that the µ-terms t and u are syntactically equivalent for some capture-avoiding renaming of µ-bound variables-e.g., µx. D(y, x) = α µz. D(y, z), but µx. C(x), µx. D(y, x), µx. D(z, x), and µy. D(y, x) are all α-disequivalent. Two µ-terms can denote the same value despite being α-disequivalent-e.g., µx. S(x) = α µy. S(S(y)).

The µ-term A [t τ ] describes a class of τ values that t and other members of t's equivalence class can take in models of E. When τ is a datatype, a cyclic µ-term describes an infeasible class of values.

The mapping A is defined as follows. With each equivalence class [u], we associate a fresh variable u of the same type as u.

  denotes the set of free variables occurring in A 's range, and A [x → t] denotes the variable-capturing substitution of t for x in A 's range. It is easy to see that the height of terms produced as a result of the unfolding is bounded by the number of equivalence classes of E, and thus the construction of A will terminate.

Example 2 Suppose that E contains four distinct equivalence classes [w], [x], [y], and [z]

such that C(w, y) ∈ [x] and C(z, x) ∈ [y] for some C ∈ F ctr . A possible sequence of unfolding steps is given below, omitting trivial entries such as [w] → w.

1. Unfold x:

  Given the mapping A , the Acyclic and Unique rules work as follows. For acyclicity, if[t] is a datatype equivalence class whose values A [t] = µx. u are cyclic (expressed by x ∈ FV(u)), then E is DC -unsatisfiable. For uniqueness, if[t], [u] are two codatatype equivalence classes whose values

C( w, C( z, C( w, C( z, . . .)))) and C( z, C( w, C( z, C( w, . . .)))), respectively.

  Acyclic, the construction of A indicates that the class of values that term t can take in models of E is infeasible. If the child nodes of E are closed derivation trees whose root nodes are the result of applying Split on t δ , by the induction hypothesis E ∪ t ≈ C j s 1 j (t), . . . , s n j

	n j

j (t) is DC -unsatisfiable for each C j ∈ F δ ctr . Since by exhaustiveness, all models of DC entail exactly one t ≈ C j s 1 j (t), . . . , s j (t) , E is DC -unsatisfiable. Otherwise, the child node of E is a closed derivation tree whose root node E ∪ t ≈ u is obtained by applying one of the rules Refl, Sym, Trans, Cong, Inject, Unique, or Single. In each of these cases, E DC t ≈ u. For Refl, Sym, Trans, Cong, this is a consequence of equality reasoning. For Inject, this is a consequence of injectivity. For Unique, the construction of A indicates that the values of t and u are equivalent in all models of E. For Single, t and u must have the same value since the cardinality of their type is one. By the induction hypothesis, E ∪ t ≈ u is DC -unsatisfiable and thus E is DC -unsatisfiable.

  ) hold initially for A . For all equivalence classes [z], each pair of constructor terms C j (t ) and C j (ū) in [z] are such that j = j , since Clash does not apply, and are such that [t ] = [ū], since Inject does not apply. Thus, A was constructed by applying a sequence of substitutions where all substitutions for variables z were uniquely of the form { z → C j ( t 1 , . . . , t n )} when [z] contains a constructor C j (t 1 , . . . , t n ). Suppose A [y] has a subterm t such that Var(t) = x. Both A [x] and the subterm t of A [y] were constructed by applying a sequence of substitutions of the form mentioned above to x. Moreover, free variables z in t that are bound in A [y] are interpreted in the expansion of t A [y] as a term

  t ≈ C 1 s 1 1 (t), . . . , s n 1 1 (t) ∨ • • • ∨ t ≈ Fig. 4 Algorithm for applying the Acyclic rule Unique(t, u): 1. Let U be a partition of the equivalence classes of E such that [t] = U [u] for distinct [t], [u] if and only if t, u have type δ ∈ Y codt , C(t 1 , . . . , t k ) ∈ [t], and C(u 1 , . . . , u k ) ∈ [u]. For each U i ∈ U: 2.2.1. Let U i be a partition of U i such that [t] = U i [u] for distinct [t], [u] if and only if -C(t 1 , . . . , t k ) ∈ [t] and C(u 1 , . . . , u k ) ∈ [u], and -[t j ] = U [u j ] for each j = 1, . . . , k.

	2. Repeat until U is unchanged:
	2.1. U := / 0.
	2.2. 2.2.2.

  Traverse([t], U, P) is such that [t] ∈ P, we know that the rule Acyclic applies to t. Otherwise, if we have yet to process [t], as indicated by the condition [t] ∈ U, then if [t] contains a constructor term C(t 1 , . . . , t k ), then we recursively call Traverse on each of [t 1 ], . . . , [t n ]. If this succeeds, we remove [t] from U.

In principle, rank-1 (top-level) polymorphism[START_REF] Blanchette | TFF1: The TPTP typed first-order form with rank-1 polymorphism[END_REF] does not raise any special difficulties. Nesting datatypes inside datatypes, and likewise for codatatypes, can be reduced to the mutual case[START_REF] Gunter | Why we can't have SML-style datatype declarations in HOL[END_REF]. So the only genuinely interesting cases missing are mixed nested (co)recursion as well as (co)recursion through a non-(co)datatype (both of which make sense, at least in a higher-order setting[START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF]).

It can be convenient to specify the same selector for several constructors associated with the same (co)datatype, as long as the argument types coincide. However, this is disallowed by SMT-LIB, so we do not consider it here.

http://lara.epfl.ch/~reynolds/JAR-CADE2015-cdt/ or http://www21.in.tum.de/~blanchet/ JAR-CADE2015-cdt/

Acknowledgment. We owe a great debt to the development team of CVC4, including Clark Barrett and Cesare Tinelli, and in particular Morgan Deters, who jointly with the first author developed the initial version of the theory solver for datatypes in CVC4. Our present and former bosses, Viktor Kuncak, Stephan Merz, Tobias Nipkow, Cesare Tinelli, and Christoph Weidenbach, have either encouraged the research on codatatypes or at least benevolently tolerated it, both of which we are thankful for. Peter Gammie and Andreas Lochbihler pointed us to useful benchmarks. Andrei Popescu helped clarify our thoughts regarding codatatypes and indicated related work. Dmitriy Traytel took part in discussions about degenerate codatatypes. Pascal Fontaine, Andreas Lochbihler, Andrei Popescu, Christophe Ringeissen, Mark Summerfield, Dmitriy Traytel, and the anonymous reviewers suggested many textual improvements. The second author's work was partially supported by the Deutsche Forschungsgemeinschaft project "Den Hammer härten" (grant NI 491/14-1) and the Inria technological development action "Contre-exemples utilisables par Isabelle et Coq" (CUIC).

Conflict does not apply, t ≈ u / ∈ F and thus [t] and [u] are distinct. Since J (t) = α A [t] and J (u) = α A [u], by Lemma 2(3), J (t) = J (u), and thus J t ≈ u.

Since F contains only equalities and disequalities, we have J F, and since E ⊆ F, we conclude that J E. CVC4 was run on each problem several times, with the support for datatypes and codatatypes either enabled or disabled. The contributions of the acyclicity and uniqueness rules were also measured, by selectively enabling or disabling the rules. Even when the decision procedure is disabled, the problems may contain basic lemmas about constructors and selectors, allowing some (co)datatype reasoning. This is especially true for problems generated using 256 lemmas. The problems with 16 lemmas put more stress on the decision procedure but are less typical of Sledgehammer-generated problems.

Distro

The results are summarized in Tables 1 and2. The decision procedure makes a difference across all three benchmark suites. For the 16-lemma problems, it accounts for an overall success rate increase of over 5%. Moreover, every aspect of the procedure, including the more expensive rules, makes a contribution. For the 256-lemma problems, the difference is much smaller, at 0.5%. Table 2 indicates that the theoretically stronger instances of the decision procedure do not always subsume the weaker ones in practice. The raw data reveal that the full procedure proved 27 goals that could not be proved without it, but failed for 17 goals that could be proved without it. This potentially points to poor interactions between the decision procedure and the quantifier instantiation module [START_REF] Reynolds | Finding conflicting instances of quantified formulas in SMT[END_REF].

Overall, four proofs were found thanks to the acyclicity rule and 17 required uniqueness. Interestingly, no proofs were lost by enabling these rules. Among the 17 proofs requiring uniqueness, some were simple arguments of the form by coinduction auto in Isabelle [START_REF] Blanchette | Truly modular (co)datatypes for Isabelle/HOL[END_REF], while others involved more elaborate reasoning, including the following example about Stern-Brocot trees: