CDSAT (Conflict-Driven Satisfiability ) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved.
bridge between arrays and linear integer arithmetic (LIA) that forces the two theories to share symbols (e.g., the theory of arrays with MaxDif [6] and LIA share 0 and ≤).
We present a new abstract approach to nondisjoint theories with bridging functions, and we exemplify it with the theory ArrL of arrays with abstract length. In ArrL, the length of an array can be an integer, but does not have to be, and the concept of an index being within bounds is abstracted into that of an index being admissible. Admissibility is expressed by the shared predicate Adm, which remains uninterpreted for ArrL, while another theory , which is not necessarily LIA, provides its interpretation. In this manner, the two theories share a minimum amount of information, namely Adm and the sorts of its arguments, indices and lengths. In ArrL, an array is interpreted as a partial updatable function, whose domain of definition is given by the set of admissible indices. We define an axiomatization and a CDSAT theory module for the theory ArrL.
We show that CDSAT is complete for this kind of nondisjoint combination (soundness and termination are preserved). The completeness of CDSAT employs the concept of a leading theory, say 1, which may be one of the theories in the union or a theory that only needs to exist in principle. 1 acts as a hub: it has the information shared between any two theories, and it sufices that each theory agrees with 1 on the shared information to have an agreement among all the theories. If the theories are disjoint, they only need to agree on equalities and the cardinalities of shared sorts. Thus, 1 has all the sorts in the union and aggregates all the cardinality constraints on the shared sorts [1, 2]. If the theories are not disjoint, they also need to agree on shared symbols other than equality.
share the predicate Adm with 1. The agreement between and 1 and the agreement between ArrL and 1 imply the agreement between and ArrL, on the interpretation of
A signature Σ is given by a set of sorts, including the sort prop of Booleans, and a set of sorted symbols, with equality symbols ≃ for all sorts ∈ . A collection = ( ) ∈ of disjoint sets of variables is available. We use and for terms, and for formulae that are the terms of sort prop. Σ[ ]-interpretations and Σ-structures are defined as usual.
of symbols in Σ, or as the class of Σ-structures that satisfy , called models of or -models. Symbols that do not appear in the axioms are free or uninterpreted. Let 1, . . . , with signatures Σ = ( , ), ∀ , 1 ≤ ≤ , be the theories to be combined. Their union is denoted ∞, with signature Σ∞ = ( ∞, ∞), for ∞ = ⋃︀ =1 and ∞ = ⋃︀ =1 . The symbols and Σ stand for any and Σ including ∞ and Σ∞. If the top symbol of a subterm of a ∞-term is not in , term is a variable for theory : term and its top symbol are dubbed Σ -foreign. Recall that ⊴ is the subterm ordering. The set fvΣ( ) of the free Σ-variables of term is the set of all ◁-maximal subterms of whose top symbol is Σ-foreign.
The simplest theory of arrays is the theory Arr0 of arrays without extensionality, which does not have axioms specifying when two arrays are equal. The theory Arr of arrays with extensionality adds to Arr0 an extensionality axiom saying that two arrays are equal if and only if they have the same elements at all indices. In this section we define a theory ArrL of arrays with extensionality and abstract length, which extends Arr0 in a diferent way, specifying diferent conditions for two arrays to be equal.
allow arrays of diferent types, including arrays of arrays, one assumes a set of basic sorts, which includes prop, and an array sort constructor, denoted ⇒, so that ⇒ is the sort of arrays with indices of sort , elements of sort , and lengths of sort . The set ArrL
The signature of ArrL includes the function symbols select : ( ⇒ )× of the sorts of ArrL is the free closure of the set of basic sorts with respect to ⇒. → for select or read, store : ( ⇒ )× ×
→ ( ⇒ ) for store or write, and len : ( ⇒ ) → that maps an array to its length len( ). Terms of the form select(, ) may be abbreviated as [ ]. The signature also features a predicate symbol Adm : × → prop, such that if is a term of sort and is a term of sort ⇒ , then Adm(, len( )) is true if index is admissible with respect to len( ). Another theory shares with ArrL the symbol Adm and the sorts and (sharing the sort is not necessary) and provides a concrete meaning of admissibility. The notion of admissibility is an abstraction that frees the theory of arrays from the commitment that lengths are positive integers and that the indices of array are the consecutive nonnegative integers in the interval [0, ) for = len( ).
Example 1. LIA interprets both the sort of lengths and the sort of indices as the set Z of the integers, and defines
Adm(, ) ↔ 0 ≤ < . A diferent theory may interpret as a set and as the powerset of , denoted ( ), and define Adm(, ) ↔ ∈ . In and this case, ∈ ( ) is the set of admissible indices, indices are not necessarily numbers, does not have to be an interval nor even an ordered set. Another theory may interpret as Z and as the set of pairs of the form (, ), where is a binary number representing the start address of the array in memory, and is an integer representing the number of admissible indices. Then, the axiom defining admissibility would be Adm(, (, )) ↔
0 ≤ < , where the start address plays no role in
characterizing the set of admissible indices. With this axiom for admissibility, we can
have two distinct arrays and with the same set of admissible indices {0, 1, 2, 3, 4}, but
len( ) = (
Let and be variables of an ⇒
sort, and be variables of sort , and be variables of sort , and and
be variables of sort . The axiomatization of ArrL
includes congruence axioms (
( ≃ ∧ ≃ ) → select(, ) ≃ select(, ),
(
Axiom (
Example 2. Picture a model of Arr, extended with an interpretation of len and Adm,
where arrays and have the same length, agree at all admissible indices, but disagree at
an index that is not admissible: ≃ is false in this model and hence the extensionality
axiom of ArrL (axiom (
inadmissible index leaves the array unchanged. Therefore, first, the length is unchanged
(axiom (
Alternatively, one can have a theory where a store at an inadmissible index in array
changes the length. This is captured by replacing axiom (
Adm(, len( )) → len(store(, , )) ≃ len( ).
(
(Adm(, len( )) ∨ ≃ ) → Adm(, len(store(, ,
Models of this theory include data structures such as finite maps and vectors (aka dynamic
arrays) which satisfy stronger versions of axiom (
(Adm(, len( )) ∨ ≃ ) ↔ Adm(, len(store(, ,
(Adm(, len( )) ∨ ≤ ) ↔ Adm(, len(store(, ,
))).
))),
(
which captures the growth of the vector as an efect of the store.
In this section we summarize the CDSAT framework and we modify it sparingly to accommodate shared predicates. CDSAT works with assignments of values to terms, including formulae that get Boolean values. Thus, CDSAT treats Boolean and first-order assignments, initial assignments and generated assignments, as uniformly as possible. The with signature Σ are provided by a conservative theory extension values for a theory
+ with signature Σ+ that adds as many constant symbols as needed to name all the individuals in the sets used to interpret the sorts of . The added constants are called -values. In this way terms and values are kept separate. Conservativity means that if a Σ-formula is -satisfiable then it is also true and false, so that true and false are -values for all . The trivial extension adds +-satisfiable. All extensions add the values only true and false. The signature of ∞ + is the union of the signatures of 1+, . . . , + arbitrary sort. A -assignment is one where all assigned values are -values. so that all values are ∞-values. We use b for true or false and c for generic values of Definition 1 (Assignment).
A set = { 1←c1, . . . , ←c } is a -assignment if for all , 1 ≤ ≤ , is a ∞-term and c is a -value of the same sort.
The set of terms that occur in as above is ( ) = { | ⊴ , 1 ≤ ≤ }. If all values in are Boolean, is a Boolean assignment. If no value in is Boolean, is a ifrst-order assignment . The flip
of a Boolean singleton assignment , written , assigns is an arbitrary variable of sort prop. We use for generic assignments, the opposite Boolean value to the same formula. Standard abbreviations are for ←true, for ←false, ̸≃ for ( ≃ )←false, ⊤ for ( ≃prop )←true, and ⊥ for ̸≃prop , where for generic singletons, for Boolean singletons, and or for ∞-assignments. An unqualified and ←c2 with c1 ̸= c2, from which CDSAT deduces ⊥ . The reason for this diference is assignment is a
∞-assignment. A -assignment is plausible if it does not contain both ←true and ←false. A plausible -assignment may contain first-order assignments ←c1 that CDSAT can generate terms 1 ≃ 2 and 1 ̸≃ 2 from terms 1 and 2 of sort , except when is prop. The exception prevents the construction of an infinite series such as 1 = ( ≃prop ), 2 = ( 1 ≃prop 1), 3 = ( 2 ≃prop 2), etc. Input assignments are assumed to be plausible and CDSAT preserves plausibility. The view that a theory has of a ∞-assignment
is made of the -assignments in , plus all equalities and inequalities between terms of a -sort that are entailed by first-order assignments in . Note that a Boolean assignment is in every theory view. A • { 1 ̸≃ 2 | 1←c1, 2←c2 are in , have sort ∈ ∖{ prop}, and c1̸=c2}. and ←c2 in such that c1 ̸= c2 and the sort of and is a sort of . A -assignment {
←c, ←c} ⊆ , then ℳ a -assignment , written ℳ | stronger than endorsing : if ℳ | also satisfies ≃ . Endorsing the -view
of is generally = , if ℳ
satisfies ≃ c for all pairs ( ←c) ∈ . If = , then ℳ also satisfies ̸≃ , for all pairs ←c1 is satisfiable if there is a , the -view of
with set of sorts and a ∞-assignment is the -assignment equal to the union of the following sets: ⊢ then |= .
= ∅).
produce inferences of the form ⊢ℐ (or ⊢ for short) where is a -assignment and is a Boolean assignment. All CDSAT theory modules include the equality inference rules in Fig. 1. CDSAT theory modules are required to be sound: if
CDSAT works with a trail Γ which is a sequence of distinct singleton assignments that are either decisions, written ? to convey guessing, or justified assignments , written ⊢ . Decisions can be either Boolean or first-order assignments. The is a set of singleton assignments that appear before justification in the trail. Input in ⊢ assignments are justified assignments with empty justification. All justified assignments are Boolean except for input first-order assignments. Given a trail Γ = 0, . . . , , the level of an assignment is levelΓ( ) = 1 + max{levelΓ( ) | < }, if is a decision, and levelΓ( ) = max{levelΓ( ) | ∈ }, if is ⊢ (where levelΓ( ) = 0 if
with a decision ? , provided it is acceptable for a -module ℐ in the -view of the trail. Definition 3 (Acceptability).
A singleton -assignment ←c is acceptable for a is relevant to in . module ℐ in a -assignment , if (i) does not assign a -value to , (ii) if ←c is first-order, there are no ℐ -inferences ′ ∪ { ←c} ⊢ℐ for ′ ⊆ and ∈ , and (iii) UndoClear Resolve UndoDecide ⟨Γ; ⊎ { }⟩ ⟨Γ; ⊎ { }⟩ ⟨Γ; ⊎ { }⟩ LearnBackjump ⟨Γ; ⊎ ⟩ −→ −→ −→ −→ =⇒ =⇒ =⇒ =⇒ Γ, ? Γ, ⊢ unsat Γ′ Γ≤ −1 Γ≤ −1, ? Γ≤ ,
⊢ Decide Deduce Fail ConflictSolve Γ Γ Γ Γ Trail rules (assume 1 ≤ ≤ ) The next three rules share the conditions: Conflict state rules (recall that ⊎ is disjoint union) if is an acceptable -assignment for ℐ in Γ ⊆ Γ, (
⊢ ), and ̸∈ Γ. if ̸∈ Γ and is in ℬ if ∈ Γ and levelΓ( if ∈ Γ, levelΓ( ∪ { } ⟨Γ; ∪ { }⟩ =⇒* Γ′ ∪ { }) = 0
) > 0, and if is a first-order decision of level > levelΓ( ) levelΓ( ′) = levelΓ( ⊎ { }
) ⊢ ⟨Γ; ∪ ⟩ if (
) ∈ Γ and for no first-order decision ′ ∈ = levelΓ( ) = levelΓ( ) = levelΓ( ′) if ( ⊢
) ∈ Γ and for a first-order decision ′ ∈ if is a clausal form of , is in ℬ , /∈ Γ, /∈ Γ, and levelΓ( ) ≤ < levelΓ( )
Condition (i) avoids multiple assignments to a term by the same theory and preserves plausibility. Condition (ii) blocks a first-order assignment that triggers an inference {
, } yielding a trivial conflict
. Condition (iii) ensures that the assigned term is relevant. The definition of relevance of a term to a theory in an assignment is the first definition that has to be changed to accommodate shared predicates . First, it makes sense than equality the latter subtlety is irrelevant. may decide a value for a term if occurs in the -view Γ of the has values for the sort of . For equality, it also makes sense that ℐ may decide ≃ if and occur in Γ , even if ≃ does not, and
for the sort of and : indeed, if
has values for their sort, ℐ can decide values for and , and glean the value of ≃ by an equality inference. For shared predicates other does not have values Definition 4 (Nondisjoint Relevance).
Given a theory with signature Σ = (, ) and a -assignment , where ( ) is the set of terms that occur in , a term is relevant to in , if either (i)
∈ ( ) and equality 1 ≃ 2 such that 1, 2 ∈ ( ), ∈ , but or (iii) is a Boolean term ( 1, . . . , ) such that : ( 1× · · · × )→prop, and for all , 1 ≤ ≤ , ∈ ( ) and ∈ . has values for the sort of ; or (ii) is an
does not have values for sort ; ∈ is a shared predicate symbol Example 3. Consider ArrL with Adm interpreted by LIA (cf. Example 1). Given assignment LIA is in = { ←3, ≃ , len( ) ≃ , ←5, select(store(, , ), ) ̸≃ }, the view of for ∪ { ̸≃ }, whereas the view of
for ArrL contains the Boolean assignments and { ̸≃ }. The term Adm(, ) does not occur in either view, but its arguments do. Thus, Adm(, ) is relevant to both LIA and ArrL by Condition (iii) in Definition 4. venture Adm(, )←false, LIA would detect a conflict.
Having the definition of
Adm, LIA can decide wisely Adm(, )←true. If ArrL were to inference
Rule Deduce expands the trail with a justified assignment ⊢ supported by a theory ⊢ for some , 1 ≤ ≤ . These deductions cover propagation or conflict detection/explanation.
a Boolean conflict:
can be derived and is on the trail. If such a conflict arises at level 0, rule Fail reports unsatisfiability. If such a conflict arises at a level greater than 0, the system enters conflict state with rule ConflictSolve . Rule Resolve transforms the conflict state until the conflict can be solved by either UndoClear or UndoDecide or LearnBackjump, producing a modified trail that ConflictSolve returns, allowing the search to resume. Trail Γ≤ is the restriction of trail Γ to its elements of level at most (cf. UndoClear, UndoDecide, and LearnBackjump). The clausal form of a Boolean of terms (in from which ℐ can 1+-model ℳ 1
As theory module inferences can generate new (i.e., non-input) terms, every theory practice, the set of input terms), basis ( ) is a finite superset of module ℐ comes with a local basis denoted basis . Given a finite set pick new terms. From the local bases it is possible to construct a finite stable global basis ℬ , where stable means basis (ℬ ) ⊆ ℬ for all , 1 ≤ ≤ (see [2] for the details of the construction). The sets produced by the local bases and hence ℬ are required to be closed, meaning ◁-closed (if is a member so is every such that ◁ ) and equality-closed (if non-Boolean terms and are members so is ≃ ). CDSAT checks that the terms assignment
CDSAT is sound if the theory modules are sound [1, Thm. 1]; and terminating, if ℬ is ifnite , closed, and contains all input terms [1, Thm. 2]. Soundness and termination are not afected by the presence of nondisjoint theories, as long as their modules are sound, generated during a derivation are in ℬ
(cf. Deduce and LearnBackjump). come with finite closed local bases, and there exists a ℬ with the required properties.
the other modules are leading-theory-complete, ℬ is stable and contains all input terms [1, Thms. 3, 4, 5]. The notions of a module being complete (for its own theory) or leadingtheory-complete do not need to be reformulated for the nondisjoint case. First, we say -assignment by adding either a -assignment that is acceptable for ℐ in (cf. Decide), or a Boolean assignment ←b such that ′ ⊢ℐ ( ←b), for ′ ⊆ , ( ←b) ∈/ , and ∈ basis( ) (cf. Deduce, Fail, and ConflictSolve ). Then, a -module ℐ is complete if whenever it cannot expand a plausible -assignment , there exists a shared terms [1, Def. 13]. Leading-theory-compatibility is the second definition that agrees with ℳ 1 on the cardinality of shared sorts and on equalities between is leading-theory-compatible with disjoint case, leading-theory-compatibility says that if ℳ 1 |= 1 for a leading-theory-complete if whenever it cannot expand a plausible -assignment , then sharing the set of terms ( ) [1, Def. 14]. In the then there exists a equality to all shared predicates.
Let 1 be the leading theory,
sharing , if for all 1+[ 1]) stand for and Σ = ( , ), 2 ≤ ≤ , and be a set of terms. 1 such that ℳ 1 |= 1 with fvΣ1 ( ∪ ) ⊆ 1, there exists a +[ ]-model ∪ ) ⊆ , such that (i) ℳ | = ; (ii) for all shared predicates ∈ 1 with : ( 1× · · · × )→prop and for all terms 1, . . . , ∈ ( ( 1, . . . , )); and (iii) for all sorts to domain ℳ 1 (so that | ℳ | = | ℳ 1 |), such that for all
of sorts 1, . . . , , ∈ , there exists a shared predicates ∈ ∩
1 with : ( 1× · · · × )→prop and for all inhabitants 1, . . . , When equality is the only shared predicate, property ( ) in the above definition reduces to ℳ 1, 2 ∈
( 1) = ℳ models interpret equality as identity. With other shared predicates, the property is stated of sort . Property ( ) reduces to | ℳ | = | ℳ 1 | for all ∈ , because all explicitly, relying on named bijections between the interpretations of a shared sort. ( 2) if and only if ℳ 1( 1) = ℳ 1( 2) for all sorts ∈ and terms
In previous work we gave a CDSAT module for theory Arr [1] and proved its
leadingtheory-completeness [2, Thm. 4]. In this section we give a CDSAT theory module ℐ ArrL
for theory ArrL (cf. Sect. 3 for Arr, ArrL and the axioms of ArrL). The reduction to clausal
form of the extensionality axiom (
) ⊢ArrL ⊥ ≃ ⊢ArrL len( ) ≃ len( ) ≃ ,
≃ , Adm(, ), ¬ Adm(, ) ⊢ArrL ⊥ ≃ ,
≃ , dif (, ) ̸≃ dif (, ) ⊢ArrL ⊥ ≃ , len( ) ≃ ,
Adm(, ), ≃ store(, ,
), select(, ) ̸≃
⊢ArrL ⊥
̸≃ ,
≃ , ≃ store(, ,
), ≃ , select(, ) ̸≃ select(, ) ⊢ArrL ⊥
len(store(, ,
)) ̸≃ len( ) ⊢ArrL ⊥
̸≃ , len( ) ≃ len( ) ⊢ArrL select(, dif (, )) ̸≃ select(, dif (, ))
̸≃ , len( ) ≃ len( ) ⊢ArrL Adm(dif (, ), len( ))
(
The first requirement when designing a CDSAT module is that its rules are sound,
which is satisfied by ℐ ArrL. The second requirement is that it is possible to define a
local basis. Rules that generate ⊥ are convenient, because they are useful for conflict
detection and they are trivial for the construction of the local basis, since it sufices
that it contains ⊤ (the flip of ⊤ is ⊥). The third requirement is that the module is
leading-theory-complete. In order to prove this property, the rules of the module must put
on the trail the terms needed for defining a model. This is why rules (
The local basis for ArrL maps any given finite set of terms to a set basisArrL( ) defined as the smallest closed set such that ⊆ , ⊤ ∈ , and: 1. For all terms 1 and 2 of sort prop that occur as subterms of terms in with select, store, len, or dif as top symbol, ( 1 ≃prop 2) ∈ ; 2. For all terms ∈ and ∈ of the same array sort, Ded(, ) ⊆ , where Ded(, ) contains precisely the terms len( ), select(, dif (, )), select(, dif (, )), Adm(dif (, ), len( )), and Adm(dif (, ), len( )).
The following reasoning shows that is finite. For Clause (
proof showing how to construct a finite global basis for a union of theories from the local bases of the component theories [2].
As arrays represent functions that can be updated, a model of Arr interprets an array as an updatable function from indices (meaning a set interpreting the sort of indices) to elements (meaning a set interpreting the sort of elements). Given generic sets and , and the set of the functions from to , we say that ⊆ is an updatable function set from to , if every function obtained by a finite number of updates to a function in is in . A model of Arr interprets an array sort as an updatable function set. A model of ArrL interprets an array as a partial updatable function, whose domain of definition is the set of admissible indices. Therefore, the cardinality of an array sort depends on the interpretation of Adm.
Definition 6 ( ArrL-suitability). A leading theory 1 is suitable for ArrL, or ArrL-suitable, if it has all the sorts in ArrL, it shares with ArrL only the equality symbols ≃ for all sorts ∈ ArrL and the symbol Adm, and for all 1-models ℳ 1 and array sorts ⇒ there exists a length-indexed collection ( ) ∈ ℳ 1 of nonempty sets such that |( ⇒ )ℳ 1 | = | ⨄︀ ∈ ℳ 1 | where is an updatable function set from = { | ∈ ℳ 1 ∧ Admℳ 1 (, )} to ℳ 1 for all ∈ ℳ 1 .
The set is the set of updatable functions that interprets the arrays of length . The functions in are partial as they are defined only on the set of admissible indices for length and not on the set ℳ 1 of all indices. Note that the interpretation of select remains nonetheless a total function, because every term select(, ) is interpreted.
Example 4. Consider the first case of Example 1. Suppose that ArrL interprets also
as Z. A leading theory that interprets , , and Adm as stipulated by LIA, and as
stipulated by ArrL is ArrL-suitable: for all ∈ Z, the set of admissible indices is
{ | ∈ Z ∧ 0 ≤ < }. Since is countably infinite for all , > 0, the cardinality of
the interpretation of ⇒ is countably infinite. Suppose that ArrL interprets as a
ifnite set of cardinality ( > 0). A leading theory that interprets , , and Adm as
stipulated by LIA, and as stipulated by ArrL is ArrL-suitable: since has cardinality
for all , > 0, the cardinality of the interpretation of ⇒ is countably infinite.
In both cases, a leading theory that interprets ⇒ as being finite is not ArrL-suitable.
Example 5. Consider the union of ArrL and the theory BV of bitvectors, where BV[ ] is
the set of bitvectors of length . Assume that BV interprets as BV[1], as BV[2], and
Adm as true everywhere except for the pairs (0, 00), (
The extension ArrL+ for ArrL may either be trivial, or add a countably infinite set of
assuming that ArrL+ is nontrivial.
Lemma 1. If is a plausible ArrL-assignment that ℐ ArrL cannot expand, for all terms of an array sort, if is in ( ), then the term len( ) is also in ( ).
Proof: By reflexivity ( ≃ ) ∈ , by rule (
needs to be concerned only with the lengths of arrays that difer. The point is that in
⇒ ), and the model construction in the proof of leading-theory-completeness of ℐ ArrL needs to define a length function as a step towards the functional interpretation of arrays. Theorem 1. Module ℐ ArrL is leading-theory-complete for all ArrL-suitable leading theories. Proof: Let be a plausible ArrL-assignment that ℐ ArrL cannot expand. We show that is leading-theory-compatible with ArrL sharing ( ). We begin by observing that every formula ∈ prop( ) is relevant to ArrL by Condition (i) of Definition 4, and therefore assigns a value to (see [2, Lemma 1, Claim 2]). For a sort other than prop, every term ∈ ( ) is relevant to ArrL by Condition (i) of Definition 4, as ArrL+ has (infinitely many) values for all sorts , , , and ⇒ . Moreover, the only ArrL-inferences using first-order assignments are equality inferences, and therefore assigns a value to every such term (see [2, Lemma 1, Claim 3]). It follows that assigns values to all terms in ( ) (†) and fvΣArrL ( ( )) = fvΣArrL ( ) (see [2, Corollary 1]). Let 1 be an ArrL-suitable leading theory, Σ1 its signature, 1+ its extension, ℳ 1 a 1+[ 1]-model such that fvΣ1 ( ) ⊆ 1 and ℳ 1 |= 1 , and ( ) ∈ ℳ 1 the length-indexed family of updatable function sets for ℳ 1 of Definition 6. We start the construction of the ArrL+[ ]-model ℳ with fvΣArrL ( ) ⊆ by interpreting • All sorts in and all variables ∈ fvΣArrL ( ) as ℳ 1 does; • The shared predicate Adm as ℳ 1 does, to get Parts (ii) and (iii) of Definition 5; • All ArrL-values c such that ( ←c) ∈ as ℳ 1 interprets ; and • All other ArrL-values arbitrarily.
We need to define how ℳ interprets symbols len, store, select, and dif . To this end, for every inhabitant of ( ⇒ )ℳ , we construct a functional interpretation mapping indices in ℳ to elements in ℳ . More precisely, we will define • A function len from ( ⇒ )ℳ to ℳ mapping arrays to lengths; • A function from ( ⇒ )ℳ to ⨄︀ ∈ ℳ 1 such that ( ) is in for = len( ), so that ( ) is an updatable function from the set of admissible indices to ℳ ; • A function from ( ⇒ )ℳ to an updatable function set from ℳ to ℳ so that ( ) is a total updatable function from ℳ to ℳ that agrees with ( ) on ; • A function dif from ( ⇒ )ℳ ×( ⇒ )ℳ to ℳ mapping pairs of arrays to indices.
symbols len, store, select, and dif , respectively. We build this interpretation so as to satisfy: 1. The axioms of ArrL so that ℳ is an ArrL+[fvΣArr ( )]-model; 2. The assignment so that ℳ | = and Part (i) of Definition 5 is fulfilled;
For (
inhabitants of ( ⇒ )ℳ that are used by ℳ 1 to interpret terms in ( ). Let be the ifnite subset of ( ⇒ )ℳ consisting of those elements such that ℳ 1( ) = for some term ∈ ( ). The first step is to define len , , and , the respective cores of len, , and that are only defined on .
1. Definition of len , , and :
Let be an element of with = ℳ 1( ) for term ∈ ( ). By Lemma 1, len( ) ∈ ( ). Model ℳ 1 sees len( ) as a variable in fvΣ1 ( ), since len is a Σ1foreign symbol. We define len ( ) = ℳ 1(len( )). Let ℛ ⊆ ℳ × ℳ be the set of index-element pairs dictated by . Formally, is the relation defined by the union of three sets: {(ℳ 1( ), ℳ 1( [ ])) | select(, ) ∈ ( ), ℳ 1( ) = } {(ℳ 1( ), ℳ 1( )) | store(, , ) ∈ ( ), ℳ 1(store(, , )) = , ℳ 1( ) ∈ len ( )} {(ℳ 1( ), ℳ 1( [ ])) | store(, , ) ∈ ( ), select(, ) ∈ ( ),
ℳ 1(store(, , )) = , ℳ 1( ) ̸= ℳ 1( )}.
In other words, ℛ is dictated by the terms in ( ) where either select is applied
to an array term that ℳ 1 interprets as or the application of store forms an array
term that ℳ 1 interprets as . Since ( ) is finite, ℛ is finite. Also, ℛ is a
functional relation from ℳ to ℳ , because otherwise ℐ ArrL could expand by
rules (
By way of contradiction, suppose that there are two elements , ∈ such that
̸= and ( ) = ( ). Since ( ) is a function in for = len ( ) and ( )
is a function in for = len ( ), the equality ( ) = ( ) means that and
have non-empty intersection. Since the collection ( ) ∈ ℳ is pairwise disjoint,
it must be = . Since , ∈ , we have = ℳ 1( ) and = ℳ 1( ) for some
terms , ∈ ( ). This means that ℳ 1 |= ̸≃ . By (†) assigns values to and ,
and therefore it also assigns a truth value b to ≃ , because otherwise an equality
inference could expand . Also, (( ≃ )←b) ∈ 1 by definition of theory view.
Since ℳ 1 |= ̸≃ and ℳ 1 |= 1 , the truth value b must be false, or, equivalently,
( ̸≃ ) ∈ . Moreover by Lemma 1, len( ) and len( ) are also in ( ), and assigns
them values by (†). Thus, assigns a truth value b′ to len( ) ≃ len( ) and so does
1 . Since len ( ) = len ( ), by definition of len we have lenℳ 1 ( ) = lenℳ 1 ( ).
Since ℳ 1 |= 1 , the truth value b′ must be true (i.e., (len( ) ≃ len( )) ∈ ).
By rule (
Since the two right hand sides are diferent, the two left hand sides are also diferent, so that ( ) ̸= ( ), a contradiction. 3. Definition of , len, , and dif : • Since is an injective function from to ⨄︀ ∈ ℳ , we can extend it to a bijection from ( ⇒ )ℳ to ⨄︀ ∈ ℳ which have the same cardinality. • For all ∈ ( ⇒ )ℳ let len( ) be the unique in ℳ such that ( ) is in . Note that for ∈ we have len( ) = len ( ). • For all ∈ ( ⇒ )ℳ , if ∈ let ( ) = ( ); otherwise, let ( ) be the function that agrees with ( ) on , where = len( ), and with everywhere else. • For all , ∈ ( ⇒ )ℳ , if , ∈ let dif (, ) = dif (, ); otherwise, if = or ( ̸= and len( ) ̸= len( )), let dif (, ) be arbitrary. If ̸= and len( ) = len( ) = , let dif (, ) = for any index ∈ such that ( )( ) ̸= ( )( ), where at least one such exists, because ̸= implies ( ) ̸= ( ) by injectivity of . 4. How ℳ interprets len, dif , select, and store for all array sorts ⇒ : • For all ∈ ( ⇒ )ℳ let lenℳ ( ) = len( ) ∈ ℳ ; • For all , ∈ ( ⇒ )ℳ let dif ℳ (, ) = dif (, ) ∈ ℳ ; • For all pairs (, ) ∈ ( ⇒ )ℳ × ℳ let selectℳ (, ) = ( )( ) ∈ ℳ ; • For all triples (, , ) ∈ ( ⇒ )ℳ × ℳ × ℳ we define storeℳ (, , ) by considering two cases with len( ) = : – If ̸∈ : let storeℳ (, , ) = ; – If ∈ : let be the function from to ℳ that maps to and every other ∈ to ( )( ) ∈ ℳ ; function is in as it difers from ( ) ∈ by one update; since is a bijection, take −1( ) which is in ( ⇒ )ℳ and set storeℳ (, , ) = −1( );
The claim holds also if ArrL+ is the trivial extension. The proof is similar, except that non-Boolean terms are not assigned ArrL-values. Leading-theory-completeness is preserved if ℐ ArrL is enriched with rules obtained from those deriving ⊥ by removing the last premise and adding its flip as conclusion (see [2, Lemma 2]).
sharing predicates. Let a predicate-sharing union of theories be a union ∞ of theories 1, . . . , , such that the signatures are disjoint or share predicate symbols, and there exists a leading theory, say 1, which has all sorts and all shared symbols in its signature.
As a consequence of generalizing leading-theory-compatibility to a predicate-sharing
union, the concept of model-describing assignment from [1, Def. 19] is generalized
accordingly. Preliminarly, given an assignment , the set sh( ) of the shared terms in
contains the left-hand sides of pairs in and all their subterms that are shared variables
or foreign terms for any theory [1, Def. 18]. An assignment is model-describing if (
Theorem 2. In a predicate-sharing union of theories, if an assignment
describing, there exists a ∞+[fv( )]-model ℳ such that ℳ | = .
is
modelProof: The proof is structured in eight short parts like that of [1, Thm. 4]. In order to
accommodate shared predicates it sufices to modify Parts (
1. Existence of a leading-theory model ℳ 1: by the hypothesis that is modeldescribing, there exists a 1+[ 1]-model ℳ ′1, with fvΣ1 ( 1 ) ⊆ 1, such that ℳ ′1 |= 1 . Note that for all , 1 ≤ ≤ , fvΣ ( ) = fvΣ ( ) ⊆ fvΣ ( sh( )) (*). Thus, we have fvΣ1 ( ) ⊆ 1, but there may be terms in fvΣ1 ( sh( )) that are not in 1. Therefore, we pick arbitrary elements in the domains of ℳ ′1 to interpret terms in fvΣ1 ( sh( ))∖ 1, if any, and we extend ℳ ′1 into a 1+[fvΣ1 ( sh( ))]-model ℳ 1 such that ℳ 1 |= 1 . 2. Existence of the other -models ℳ : by the hypothesis that is model-describing, for all , 2 ≤ ≤ , there exists a and hence fvΣ ( sh( )) ⊆ +[ ]-model ℳ where fvΣ ( ∪ sh( )) ⊆
by (*), with the following properties: (i) ℳ to domain ℳ 1 , such that for all shared predicates ℳ |= , (ii) for all sorts ∈ , there exists a bijection from domain ∈ ∩ 1 with : ( 1× · · · × )→prop: (iii) for all terms 1, . . . , ∈ sh( ) of sorts 1, . . . , ,
( ( 1, . . . , )), and (iv) for all inhabitants 1, . . . , of 3. Bijection between any ℳ and ℳ 1
: For all , 1 ≤ ≤ , we construct a collection of bijections : ℳ → ℳ 1 indexed satisfies the additional property ( by ∈ , that satisfies the same properties as the of sort .
ℳ ( )) = ℳ 1( ) for all shared terms ∈ sh( ) ( ) ∈ collection, but also
Φ such that, if Ψ( ) (ℳ ( )) ̸= ℳ Let 1 (resp. ) be the (finite) subset of ℳ 1 (resp. ℳ ) consisting of those inhabitants of the form ℳ 1( ) (resp. ℳ
( )) for some term in sh( ).
For a family ( ) compatibility, let Ψ( ) ∈ of bijections satisfying the conditions of leading-theory
∈ be the (finite) number of terms in sh( ) such that Ψ( )
∈ .
Assume (ℳ The family Φ( ) where
( ) = 1, Hence, Ψ(Φ( ) ∈
∈ properties (from leading-theory compatibility) as ( ) ∈ ity, until we obtain a family ( ) We keep applying Φ to the family ( )
∈ from the leading-theory compatibilthat also satisfies the additional property ) < Ψ( )
∈ . Also note that Φ( ) ( )) ̸= ℳ 1( ). Let 1 = (ℳ
( )) and let = ( )−1(ℳ ∈ is the family that updates ( )
∈ by replacing by , (ℳ ( )) = ℳ 1( ), and for every other , ( ) = ( ).
1( )). ∈ with Ψ( )
∈ > 0, then Ψ(Φ( ) ∈ = 0.
∈ ) < does. ∈ satisfies the same
( ℳ ( )) = ℳ
1( ) for all shared terms ∈ sh( ) of sort .
Given a predicate-sharing union of theories 1, . . . , , a collection of theory modules ℐ 1, . . . , ℐ for 1, . . . , is complete, if module ℐ 1 is complete for the leading theory, and the generalized version of [1, Thm. 3], where an assignment modules ℐ ’s, 2 ≤ ≤ , are leading-theory-complete. With this assumption, one shows is in ℬ if ( ←c) ∈ implies ∈ ℬ . is unchanged.
Theorem 3. In a predicate-sharing union of theories equipped with a complete collection of theory modules and a stable global basis ℬ , for all input assignments in ℬ , whenever a CDSAT derivation from
halts in a state Γ other than unsat, Γ is model-describing.
Theorem 4 (Completeness). In a predicate-sharing union of theories equipped with a complete collection of theory modules and a stable global basis ℬ , for all input assignments in ℬ , whenever a CDSAT derivation from halts in a state Γ other than unsat, there exists a ∞+[fv(Γ)]-model ℳ such that ℳ | = Γ and hence ℳ | = (as ⊆ Γ).
The equality-sharing method (aka Nelson-Oppen scheme) yields a decision procedure for the satisfiability of a conjunction of literals in a union of theories, by combining the respective decision procedures for the component theories [7]. The integration of the equality-sharing method in the CDCL( ) transition system1 yields a decision procedure for the satisfiability of a quantifier-free formula in a union of theories [ 11, 12]. The theories are required to be disjoint and stably-infinite , where a theory is stably-infinite if every -satisfiable formula has a -model with countably infinite domain.
Polite theory combination (e.g., [13, 14, 15, 16]) extends the equality-sharing method so as to combine a non-stably-infinite theory with a polite theory. Politeness is a stronger cardinality requirement than stable infiniteness, and in general the theories are still required to be disjoint. However, polite theory combination was generalized [5] to the nondisjoint case represented by the theories of absolutely free data structures with bridging functions, which are polite [5]. The theory of arrays with extensionality is polite [13], but arrays are not an absolutely free data data structure with constructors and selectors.
applying a superposition-based inference system to the axioms and the target formula. If superposition is a decision procedure for each of the component theories, it is a decision procedure for their union, provided the theories are disjoint and variable-inactive [17].
decidable by superposition [18] and is variable-inactive [17]. This approach was extended to unions of theories that share a theory of counter arithmetic [19, 20]. However, there are theories, such as arithmetic or bitvectors, that do not lend themselves to reasoning by generic theorem proving.
Therefore, the CDCL(Γ + ) transition system2 integrates a superposition-based inference system (the Γ parameter) in the CDCL( ) transition system, with the modelbased theory combination version [22] of equality sharing. The resulting method can reason in a union of theories comprising both built-in and axiomatized theories, provided the theories are disjoint and either stably-infinite (for the built-in theories) or variable-inactive (for the axiomatized theories). CDCL(Γ+ ) is a semidecision procedure in general, but it may yield decision procedures by employing speculative axioms [21]. A survey of the methods mentioned up to here appeared [23].
1The original name is DPLL( ) [8], but the recent literature uses CDCL( ), since the DPLL (DavisPutnam-Logemann-Loveland) [9] and CDCL (Conflict-Driven Clause Learning) [ 10] procedures have been recognized as distinct. 2Here too the original name is DPLL(Γ+ ) [21] and the renaming follows that of DPLL( ). for CDCL with those for another conflict-driven decision procedure. CDSAT [ 1, 2] generalized MCSAT to generic unions of disjoint theories, accommodating both conflictdriven and non-conflict-driven decision procedures. Stable infiniteness is not required, because an agreement on the cardinalities of shared sorts is reached via a leading theory.
infinite cardinality to the interpretation of all sorts other than prop.
problem of enriching the theory of arrays with extensionality with a notion of length of an array. Previous approaches considered this problem in the case where the indices of an array form an interval in a linearly ordered set.
bounded equality of two arrays as having equal elements at all indices between a lower bound and an upper bound. The resulting axiomatization belongs to the array property fragment, whose decision procedure reduces the problem to reasoning about uninterpreted functions, LIA, and the theory of the array elements [25].
The theory of arrays with MaxDif [6] is parametrized with respect to a theory of indices that is required to extend the theory of linear orderings with an element 0. LIA, LRA, and the theory IDL of integer diference logic (i.e., the theory with 0, successor, predecessor, and the ordering), satisfy this requirement. The theory of arrays with MaxDif features a symbol ⊥ for the undefined element and a symbol for the array that has element ⊥ at all indices. The axioms impose that an array has element ⊥ at all indices smaller than 0, and that dif (, ) is the largest index where and difer and 0 otherwise. Thus, the length of an array is given by dif (, ). The theory of arrays with MaxDif and the theory of indices need to share the symbols for the element 0 and for the ordering.
abstract length features an abstract admissibility predicate Adm for array indices. This predicate can be interpreted in such a way that the indices of an array form an interval in a linearly ordered set, but it does not have to. Thanks to this abstraction, ArrL only needs to share the symbol Adm with another theory and with the leading theory (these two theories may coincide, but they do not have to). Thus, it sufices to extend
only minimal changes to the CDSAT framework of definitions and none to the CDSAT transition system itself. We proved that CDSAT is complete for predicate-sharing unions.