Given the list of drivers for various segments of a variable, turn them into a single svex comprising that variable's full assignment.

- Signature
(segment-driverlist-resolve x) → value

- Arguments
`x`—Guard (segment-driverlist-p x) .- Returns
`value`—Type (svex-p value) .

This works in three main steps: sort the drivers by LSB and width, resolve each overlap of multiple drivers into a combined driver so that all drivers are nonoverlapping, and finally concatenate the value expressions of this nonoverlapping list of drivers into a single expression.

The complicated part is resolving overlapping drivers; see segment-driverlist-deoverlap.

**Function: **

(defun segment-driverlist-resolve (x) (declare (xargs :guard (segment-driverlist-p x))) (let ((__function__ 'segment-driverlist-resolve)) (declare (ignorable __function__)) (b* ((sort (segment-drivers-sort (segment-driverlist-fix x))) (deoverlap (segment-driverlist-deoverlap 0 sort))) (disjoint-segment-drivers->svex deoverlap))))

**Theorem: **

(defthm svex-p-of-segment-driverlist-resolve (b* ((value (segment-driverlist-resolve x))) (svex-p value)) :rule-classes :rewrite)

**Theorem: **

(defthm vars-of-segment-drivers-insert (implies (and (not (member-equal v (segment-driver-vars elt))) (not (member-equal v (segment-driverlist-vars x)))) (not (member-equal v (segment-driverlist-vars (segment-drivers-insert elt x))))))

**Theorem: **

(defthm vars-of-segment-drivers-insertsort (implies (and (not (member-equal v (segment-driverlist-vars x)))) (not (member-equal v (segment-driverlist-vars (segment-drivers-insertsort x))))))

**Theorem: **

(defthm vars-of-segment-driverlist-resolve (b* ((acl2::?value (segment-driverlist-resolve x))) (implies (not (member-equal v (segment-driverlist-vars x))) (not (member-equal v (svex-vars value))))))

**Theorem: **

(defthm segment-driverlist-resolve-of-segment-driverlist-fix-x (equal (segment-driverlist-resolve (segment-driverlist-fix x)) (segment-driverlist-resolve x)))

**Theorem: **

(defthm segment-driverlist-resolve-segment-driverlist-equiv-congruence-on-x (implies (segment-driverlist-equiv x x-equiv) (equal (segment-driverlist-resolve x) (segment-driverlist-resolve x-equiv))) :rule-classes :congruence)

- Segment-driverlist-deoverlap
- Resolve overlapping elements of an ordered list of segment driver objects, resulting in an ordered, nonoverlapping list.