CDSAT for nondisjoint theories with shared predicates: arrays with abstract length

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.