Free Data Structures are nite semantic trees modulo equational axioms that are useful to represent classical data structures such as lists, multisets and sets. We study the satis ability problem when free data structures are combined with bridging functions. We discuss the possibility to get a combination method a la Nelson-Oppen for these particular non-disjoint unions of theories. In order to handle satis ability problems with disequalities, we investigate a form of su cient surjectivity for the bridging functions.
The theory of Absolutely Free Data Structures (AFDS) corresponds to the theory of nite
syntactic trees axiomatized by Injectivity, Acyclicity, and Disjoint Constructors. The
combination with a bridging function can be handled using a locality approach [
Following the work on AFDS [
Our approach is based on the reduction of the satis ability in combined theories to the
satis ability in individual theories. Our procedure extends the one used for AFDS [
The di culty of the approach is related to the surjectivity of the bridging function. A form
of su cient surjectivity [
This work is the opportunity to reuse the constraint solving techniques known for tree
algebras, e.g., uni cation and matching procedures to solve equalities. In our approach,
disunication would be needed [
We assume the reader has some basic familiarities with equational theories and equational
uni cation [
Given a set E of -axioms (i.e., pairs of -terms, denoted by l = r), the equational theory =E is the congruence closure of E under the law of substitutivity. By a slight abuse of terminology, E will be often called an equational theory. An axiom l = r is regular if V ar(l) = V ar(r).
A -equality is a pair of -terms denoted by s = t. An E-uni cation problem is a set of -equations, = fs1 = t1; : : : ; sm = tmg. The set of variables of is denoted by V ar( ). When t1; : : : ; tm are ground, is called a matching problem. A solution to an E-uni cation problem , called an E-uni er , is a substitution such that si =E ti for all 1 i m. A decision procedure for E-uni cation is a decision procedure returning true if and only if the input E-uni cation problem admits an E-uni er. E-uni cation is said to be nitary if any E-uni cation problem admits a (computable) nite complete set of E-uni ers.
A at equality is either of the form t0 = t1 or t0 = f (t1; : : : ; tn) where each term t0; : : : ; tn is a variable or a constant. A disequality t0 6= t1 is at when each term t0; t1 is a variable or a constant. A at literal is either a at equality or a at disequality. For n distinct variables x1; : : : ; xn, the set of literals fxi 6= xj j i 6= j; i; j = 1; : : : ; ng is denoted by fx1 6= 6= xng.
A set of equalities = fxk = tkgk2K is a solved form if xk is a variable occurring only once in for each k 2 K. Note that a solved form corresponds to a most general E-uni er: it is not necessarily at, but using attening, we can obtain an equivalent at dag solved form. For instance, the attening of fv = c(u(e); y)g is the dag solved form fv = c(x; y); x = u(e)g. Roughly speaking, a dag solved form is a set of (acyclic) solved equalities leading to a solved form by variable replacement. 3
In this paper, we focus on data structure theories constructed from three operators: A binary operator c, which is not necessarily absolutely free: it may satisfy some equational properties; A unary operator u to construct a singleton structure;
A constant nil to denote the empty structure.
De nition 1. A binary constructor-based signature is of the form fc : struct
struct ! struct; nil : struct; u : elem ! structg
To simplify the notation, we often write c(e; x) instead of c(u(e); x), by assuming that e; e1; : : : ; en denote only elem-sorted variables. We may use an in x notation to write e [ x instead of [(e; x).
De nition 2. Let be a binary constructor-based signature. Given an equational -theory E, F DSE denotes the class of -structures A such that structA = T ( [ elemA)= =E . De nition 3 (Standard term). Let be a binary constructor-based signature. A structsorted -term is said to be standard if it contains no struct-sorted variables.
In this paper, we focus on regular theories whose axioms do not involve the unary operator u. We are interested in the following regular axioms: Associativity (A) (X [ Y ) [ Z = X [ (Y [ Z), Commutativity (C) X [ Y = Y [ X, Right Unit (RU ) X [ ; = X, Left Unit (LU ) ; [ X = X, and Idempotency (I) X [ X = X. But the Nilpotency (N ) X X = 0 is not regular and will not be considered. In the following, we consider any combination of the above regular axioms, such as
AU = A [ LU [ RU; AC = A [ C; ACU = AC [ LU; ACU I = ACU [ I Besides these regular theories, we also consider two special non-regular ones involving the unary operator u, related to positive integers and booleans.
Given a binary constructor-based signature = fc : struct struct ! struct; nil : struct; u : elem ! structg, a -structure A is a standard (positive integer) N-interpretation if structA = N, c is interpreted in A as the addition, A[nil] = 0 and for any a 2 elemA, A[u](a) = 1. Analogously, a -structure A is a standard (boolean) B-interpretation if structA = B, c is interpreted in A as the disjunction, A[nil] = ? and for any a 2 elemA, A[u](a) = >. Standard N-interpretations and standard B-interpretations can be viewed as models of respectively two free data structures:
EN = AC(+) [ f8X: X + 0 = Xg [ f8V; W: 1(V ) = 1(W )g
EB = AC(_) [ f8X: X _ ? = X; X _ X = Xg [ f8V; W: >(V ) = >(W )g Proposition 1. Any model of F DSEN (resp., F DSEB ) is isomorphic to a standard N-interpretation (resp., B-interpretation).
Obviously, F DSEN -satis ability and F DSEB -satis ability are decidable.
For an arbitrary equational theory E, F DSE -satis ability and E-uni cation can be related as follows: Proposition 2. A set of equalities is satis able in F DSE if and only if it is E-uni able.
Moreover, an E-uni cation algorithm computing most general E-uni ers is su cient to check E-equality and so to check the satis ability of disequalities, since an in nite interpretation domain for the elem sort can be chosen.
Proposition 3. F DSE -satis ability is decidable if a nitary E-uni cation algorithm is known. 4
In a way similar to [
De nition 4. ( [
Tf = 8 f (c(X; Y )) < f (u(V )) : f (nil) = = = fc(f (X); f (Y )) fu(V ) fnil where fc; ; fu; fnil are t-terms of respective arities 2; 1; 0.
The term rewrite system F of a bridging theory Tf is F = ff (l) ! r j f (l) = r 2 Tf g.
The term rewrite system (for short, TRS) of a bridging theory Tf is convergent. Let 1 and 2 be two binary constructor-based signatures sharing only the elem sort. The non-shared sort in i is denoted by structi for i = 1; 2. Let Tf be a bridging f -theory between signatures = 1 and t = 2, where struct = struct1 and t = struct2. Assume an equational i-theory Ei for i = 1; 2. The bridging theory Tf is said to be E1-compatible in E2 if, for any l = r 2 E1 we have f (l) #F =E2 f (r) #F .
Example 1. Consider E1 = f(X [ Y ) [ Z = X [ (Y [ Z); X [ Y = Y [ X; X [ ; = Xg and E2 = EN. The theory E1 corresponds to multisets of elements and the bridging function computing the number of elements in a multiset is given by the bridging theory
Tf = ff (X [ Y ) = f (X) + f (Y ); f (feg) = 1; f (;) = 0g:
(f (X) + f (Y )) + f (Z) =E2 f (X) + (f (Y ) + f (Z)) f (X) + f (Y ) =E2 f (Y ) + f (X) f (X) + 0 =E2 f (X)
Let E10 = E1 [ fX [ X = Xg. We remark that Tf is not E10-compatible in E2. However, given E20 = EB, the bridging theory
Tg = fg(X [ Y ) = g(X) _ g(Y ); g(feg) = >; g(;) = ?g is E10-compatible in E20. Indeed, E10 allows us to represent sets of elements. The bridging function g returns > if the input set is non-empty, and ? otherwise.
The notion of compatibility is required to get a consistent combined theory: De nition 5. Assume Tf is E1-compatible in E2. Tf [E1; E2] denotes the class of f -structures A such that A 1 2 F DSE1 , A 2 2 F DSE2 , and A j= Tf .
From now on, we assume that T = Tf [E1; E2], and Ti = F DSEi for i = 1; 2. By this de nition, we have T = T1 [ Tf [ T2. 5
The decision procedure works as a classical Nelson-Oppen combination procedure. As usual, the input set of literals is rst puri ed to get a separate form, by introducing fresh variables. Then, we may need to perform some guessing over the fresh variables in order to guarantee the existence of a combined model. In the classical Nelson-Oppen combination procedure, the guessing phase only enumerates the arrangements over the shared variables. In our context, we may need an additional guessing to explore possible values taken by the bridging function. We want to focus on cases where only nitely many guesses are su cient to get a complete procedure.
De nition 6. A set of literals ' is in separate form if ' = '1 [ 'elem [ '2 [ 'f where: '1 contains only at struct1-sorted literals 'elem contains only elem-sorted literals '2 contains only struct2-sorted literals 'f contains only at equalities of the form fx = f (x), where fx denotes a variable associated to f (x), such that fx and f (x) occur once in 'f and each variable of sort struct1 in '1 occurs in 'f .
The sets of literals '1 [ 'elem and '2 [ 'elem are called respectively the 1-component and the 2-component of '.
It is easy to convert any set of literals into an equisatis able separate form ' by introducing fresh variables to denote impure terms. In order to take into account the axioms of Tf , we need additional 2-equalities obtained by encoding the at equalities in '1.
De nition 7. Given a bridging theory Tf , the target encoding of a set of at struct1-sorted equalities ' is the set of struct2-sorted equalities
CP' =
ffv = fc(fx; fy) j v = c(x; y) 2 'g [ ffv = fu(e) j v = u(e) 2 'g [ ffv = fnil j v = nil 2 'g [ ffv = fx j v = x 2 'g
When a separate form ' contains only at struct1-equalities corresponding to a dag solved form, the target encoding of this dag solved form is su cient to reduce T -satis ability into T2-satis ability: Proposition 4. Let ' = '1 [ 'elem [ '2 [ 'f be a set of literals in separate form such that '1 is a dag solved form. The formula ' is T -satis able if and only if 'elem [ '2 [ CP'1 is T2-satis able.
The problem of considering struct1-literals including both equalities and disequalities is much more complicated. We have investigated several possible scenarios. 5.1
Theory of Integers as Target
In a rst case, we can assume that the target is the theory of integers, and that the source
admits a uni cation algorithm to solve the equalities. Consider f de nes the size of a data
structure. We introduce a guessing of nitely many range constraints [
This guessing phase leads to a T -equivalent disjunction of separate forms, each of them being T -satis able if and only if its 1-component and its 2-component are respectively T1-satis able and T2-satis able.
Proposition 5. Consider E1 is included in AC(c) [ fc(X; nil) = X; c(nil; X) = Xg, E2 = EN and Tf = ff (c(X; Y )) = f (X) + f (Y ); f (u(e)) = 1; f (nil) = 0g. For any separate form ' = '1 [ 'elem [ '2 [ 'f such that '1 is a dag solved form together with at disequalities, there exists a computable T -equivalent disjunction of separate forms Wk2K 'k such that ' is T satis able if and only if there exists some k 2 K such that the i-component of 'k is Ti-satis able for each i 2 f1; 2g.
Example 2. Assume E1 = AC(]) [ LU (;). Consider the separate form ' = 8< z = x ] y; x = e ] v; y = e ] w; x 6= y =9
fz = 2; fz = fx + fy; fx = 1 + fv; fy = 1 + fw
: fx = f (x); fy = f (y); fz = f (z); fv = f (v); fw = f (w) ;
We can check that ' is T -unsatis able by considering the following cases: (1) fv > 0; fw > 0,
(2) fv = 0; fw > 0, (3) fv > 0; fw = 0, (4) fv = 0; fw = 0. For the cases (1), (2) and (3), we
get the unsatis ability in T2. The case (4) fv = 0; fw = 0 is T2-satis able. Adding v = ; and
w = ; to '1 leads to x = feg and y = feg, which contradicts x 6= y.
In the general case, we need a form of su cient/in nite surjectivity in order to satisfy problems
of the form x1 6= 6= xn; f (x1) = = f (xn). We have studied in [
De nition 8 (Measure). Let be a binary constructor-based signature and E an equational -theory. A measure for E is a mapping from standard -terms to N such that for any standard
-terms s and t, s =E t implies (s) = (t); for any standard
-term s and any substitution , (s ) = (s); for any k 2 N and for ./ in f=; g, the constraint (x) ./ k can be equivalently expressed as a constraint in F DSE of the form (9v : x = t ^ '), where v = V ar(t), x 2= v, ' is a conjunction of disequalities between elem-variables in v, and t is standard if ./ is =. Example 3. There exists a very natural measure for the following equational theories: If E = A( ) [ fX nil = X; nil X = Xg, then can be chosen as the number of elemoccurrences of a list. The constraints (x) = k and (x) k can be respectively encoded into 9e1; : : : ; ek : x = u(e1) u(ek) and 9y; e1; : : : ; ek : x = u(e1) u(ek) y If E = AC(]) [ fX ] ; = Xg, then can be chosen as the number of elem-occurrences of a multiset. The constraints (x) = k and (x) k can be respectively encoded into 9e1; : : : ; ek : x = u(e1) ] ] u(ek) and 9y; e1; : : : ; ek : x = u(e1) ] ] u(ek) ] y If E = AC([) [ fX [ X = X; X [ ; = Xg, then can be chosen as the cardinality of a set. The constraints (x) = k and (x) k can be respectively encoded into 9e1; : : : ; ek : x = u(e1) [ [ u(ek) ^ e1 6= 6= ek and 9y; e1; : : : ; ek : x = u(e1) [ [ u(ek) [ y ^ e1 6= 6= ek If E = EN, then can be chosen as the identity on N. The constraints (x) = k and (x) k can be respectively encoded into x = k and 9y : x = k + y.
The de nition of gently growing is introduced in [
De nition 9. Let T be a theory de ned as a class of structures in Tf [E1; E2] and a measure for E2. For any A 2 T and any standard 2-term s, FA 1(s) = ft j A[f ](t) = A[s]g. The bridging function f is gently growing in T w.r.t if 1. for any A 2 T and any standard 2. for any A 2 T and any standard 2-term s, FA 1(s) 6= ;; 2-terms s and t, (s) < (t) implies jFA 1(s)j < jFA 1(t)j; 3. for any natural n > 1 there exists a computable k such that, for any standard if (s) k, then for any A 2 T , jFA 1(s)j n; if (s) < k, then one can compute a nite non-empty set F 1(s) of standard such that
_ t2F 1(s) T j= f (x) = s () (9v : x = t) where v = Var (F 1(s))
We now introduce a class of satis ability problems including at struct1-sorted disequalities together with particular dag solved forms.
De nition 10 (Isolated variable, standard variable). Let ' be a dag solved form and let be the substitution corresponding to the solved form obtained by variable replacement. A variable x is isolated in ' if x is a variable. A variable x is standard in ' if x is a standard term.
We consider dag solved forms extended with disequalities x 6= y such that x; y are both standard or both isolated.
Proposition 6. Consider a theory T = Tf [E1; E2] such that f is gently growing in T with respect to a measure for E2. Let ' be any separate form
' = '1 [ 'elem [ '2 [ 'f such that '1 is a dag solved form together with at disequalities x 6= y where x; y are both standard or both isolated. There exists a computable T -equivalent disjunction of separate forms Wk2K 'k such that ' is T -satis able if and only if there exists some k 2 K such that the i-component of 'k is Ti-satis able for each i 2 f1; 2g.
Example 4. Consider the bridging function f computing the set of elements in a multiset. Consider the separate form ' = 8< vfx==xf]y;yf;vx =6=fyx [ fy; fv = feg 9=
: fx = f (x); fy = f (y); fv = f (v) ; Using the formula ' ^ (fx = ; _ fx = e0 [ v0), we get the T -satis ability of ' thanks to the branching fx = e0 [ v0. Indeed, ' is T -satis able by considering for instance x = e ] e and y = e ] e ] e. 6
In this paper, we have studied the problem of combining satis ability procedures for the union T of two free data structure theories T1 and T2 connected by a bridging theory Tf . We have identi ed some basic propositions to solve the T -satis ability problem in a modular way when the source component of the input is already in solved form. As a pre-processing step, applying a uni cation algorithm is a natural way to compute the expected solved forms. In the case of Proposition 6, the considered solved forms can be obtained, for instance, by applying a matching algorithm on particular equations with one standard (ground) side.
The (combined) data structure theory T involves a free sort elem. The next step is to
consider the combinability of T with an elem-sorted theory Telem. In the easy case, T and
Telem are stably in nite, and we can rely on the classical Nelson-Oppen combination method.
Actually, all the theories T1, T2 and T = T1 [ Tf [ T2 studied in this paper are stably in nite.
In the general case, a politeness property [
The technical propositions stated in this paper will allow us to show the politeness of some particular T -satis ability problems. Hence, this will be a way to identify signi cant cases for which a combination method a la Nelson-Oppen will compute the right answer when it returns satis able.
Acknowledgements. We are very grateful to Paula Chocron and Pascal Fontaine for their
collaboration on the design of new combination methods for SMT solving [7{9]. This work on
FDS has been made possible thanks to the joint study of the AFDS case [