new datatype API, PART 3

shingarov · Sep 20, 2024 · fabdf91 · fabdf91
1 parent 603083e
commit fabdf91
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 0 deletions.
diff --git a/src/Z3/Z3Constructor.class.st b/src/Z3/Z3Constructor.class.st
@@ -4,7 +4,26 @@ Class {
 	#category : #'Z3-Core'
 }
 
+{ #category : #'instance creation' }
+Z3Constructor class >> name: constructorName recognizer: recognizerName fields: fields referencing: sortRefs [
+	^Z3Context current
+				mkConstructor: constructorName
+				recognizer: recognizerName
+				fields: fields
+				referencing: sortRefs
+]
+
 { #category : #'initialization & release' }
 Z3Constructor >> delete [
 	Z3 del_constructor: ctx _: self
 ]
+
+{ #category : #accessing }
+Z3Constructor >> numFields [
+	^Z3 constructor_num_fields: ctx _: self
+]
+
+{ #category : #accessing }
+Z3Constructor >> query [
+	^Z3Context current queryConstructor: self
+]
diff --git a/src/Z3/Z3ConstructorList.class.st b/src/Z3/Z3ConstructorList.class.st
@@ -4,6 +4,11 @@ Class {
 	#category : #'Z3-Core'
 }
 
+{ #category : #'instance creation' }
+Z3ConstructorList class >> withAll: constructors [
+	^Z3Context current mkConstructorList: constructors
+]
+
 { #category : #'initialization & release' }
 Z3ConstructorList >> delete [
 	Z3 del_constructor_list: ctx _: self

diff --git a/src/Z3/Z3Context.class.st b/src/Z3/Z3Context.class.st
@@ -149,6 +149,32 @@ Z3Context >> mkBvSort: length [
 	^ Z3 mk_bv_sort: self _: length
 ]
 
+{ #category : #'API wrappers' }
+Z3Context >> mkConstructor: constructorName recognizer: recognizerName fields: fields referencing: sortRefs [
+	^Z3
+		mk_constructor: self
+		_: constructorName toZ3Symbol
+		_: recognizerName toZ3Symbol
+		_: fields size
+		_: ((fields collect: #key) collect: #toZ3Symbol)
+		_: (fields collect: #value)
+		_: sortRefs
+]
+
+{ #category : #'API wrappers' }
+Z3Context >> mkConstructorList: constructors [ 
+	^Z3 mk_constructor_list: self _: constructors size _: constructors
+]
+
+{ #category : #'API wrappers' }
+Z3Context >> mkDatatype: name constructors: constructors [
+	^Z3
+		mk_datatype: self
+		_: name toZ3Symbol
+		_: constructors size
+		_: constructors
+]
+
 { #category : #'API wrappers' }
 Z3Context >> mkDistinct: astArray [
 	^ Z3 mk_distinct: self _: astArray size _: astArray
@@ -335,6 +361,22 @@ Z3Context >> parseSmtlib2String: aString [
 
 ]
 
+{ #category : #'API wrappers' }
+Z3Context >> queryConstructor: aZ3Constructor [
+	| constructorDeclArray testerDeclArray accessorsArray |
+	constructorDeclArray := Array new: 1.
+	testerDeclArray := Array new: 1.
+	accessorsArray := Array new: aZ3Constructor numFields.
+	Z3
+		query_constructor: self
+		_: aZ3Constructor
+		_: aZ3Constructor numFields
+		_: constructorDeclArray
+		_: testerDeclArray
+		_: accessorsArray.
+	^{ constructorDeclArray anyOne. testerDeclArray anyOne. accessorsArray }
+]
+
 { #category : #'initialization & release' }
 Z3Context >> release [
 	"In case #release sent to current global context, we have to flush it first