diff --git a/src/Z3/Z3DatatypeSort.class.st b/src/Z3/Z3DatatypeSort.class.st
index 2322c68ef..dc35817b2 100644
--- a/src/Z3/Z3DatatypeSort.class.st
+++ b/src/Z3/Z3DatatypeSort.class.st
@@ -53,6 +53,16 @@ Z3DatatypeSort >> accessor: i idx: j [
 	^ Z3 get_datatype_sort_constructor_accessor: ctx _: self _: i _: j
 ]
 
+{ #category : #accessing }
+Z3DatatypeSort >> accessorNamed: aString [
+	^self allAccessors detect: [ :f | f name = aString ]
+]
+
+{ #category : #accessing }
+Z3DatatypeSort >> allAccessors [
+	^(self structure values collect: #third) concat
+]
+
 { #category : #'type theory' }
 Z3DatatypeSort >> cast: val [
 	^val toDatatype: self
@@ -66,11 +76,23 @@ Z3DatatypeSort >> constructor: idx [
 	^ Z3 get_datatype_sort_constructor: ctx _: self _: idx
 ]
 
+{ #category : #accessing }
+Z3DatatypeSort >> constructorNamed: aString [
+	^self constructors detect: [ :c | c name = aString ]
+]
+
 { #category : #accessing }
 Z3DatatypeSort >> constructors [
 	^(1 to: self numConstructors) collect: [ :i | self constructor: i-1 ]
 ]
 
+{ #category : #accessing }
+Z3DatatypeSort >> fieldsOf: constructorNameString [
+	| c_r_fs |
+	c_r_fs := self structure at: constructorNameString.
+	^c_r_fs third
+]
+
 { #category : #accessing }
 Z3DatatypeSort >> getTupleSortFieldDecl: i [
 	^Z3 get_tuple_sort_field_decl: ctx _: self _: i
@@ -125,6 +147,35 @@ Z3DatatypeSort >> recognizer: idx [
 	^ Z3 get_datatype_sort_recognizer: ctx _: self _: idx
 ]
 
+{ #category : #accessing }
+Z3DatatypeSort >> recognizerFor: constructorNameString [
+	| c_r_fs |
+	c_r_fs := self structure at: constructorNameString.
+	^c_r_fs second
+]
+
+{ #category : #accessing }
+Z3DatatypeSort >> recognizers [
+	^(1 to: self numConstructors) collect: [ :i | self recognizer: i-1 ]
+]
+
+{ #category : #accessing }
+Z3DatatypeSort >> structure [
+	"Answer a Dictionary keyed by constructor names.
+	 Each value is a triple, { constructor . recognizer . accessors }.
+	 Constructor is a Z3FuncDecl of the injection morphism.
+	 Recognizer is a Z3FuncDecl :: D→𝔹.
+	 Accessors is an Array of Z3FuncDecls :: D→F where F is the field's sort."
+	^Dictionary newFromAssociations:
+	((1 to: self numConstructors) collect: [ :i |
+		| constructor recognizer accessors |
+		constructor := self constructor: i-1.
+		recognizer := self recognizer: i-1.
+		accessors := (0 to: constructor arity - 1) collect: [ :j | self accessor: i-1 idx: j ].
+		constructor name -> { constructor . recognizer . accessors }
+	])
+]
+
 { #category : #accessing }
 Z3DatatypeSort >> tupleFields [
 	^(1 to: self getTupleSortNumFields) collect: [ :j | self getTupleSortFieldDecl: j-1 ]