[Z3] (Re)introduce MonomorphizedDataDecl mid-level Datatype API

PR#351 ("Overhaul Z3-level Datatype API") has removed PyZ3-style "dynamic attributes" of Z3 Datatypes in favor of a strictly-disciplined API 100% faithful to Nikolaj's C API and proposed to "jump up" to LH-like DataDecl for the next-higher level.

This is all good; but it misses one numance, namely how Z3 implements SMTLIB's "declare-datatypes" via instantiate_datatype() in pdecl.cpp.  When PR#351 removed "dynamic attributes", it also removed some good stuff, i.e. recursive-sort-indexing.  This commit reintroduces MonomorphizedDataDecl: similar to Z3Datatype minus the "dynamic" aspect.

src/Z3-Tests/MonomorphizedDataDeclTest.class.st

@@ -0,0 +1,108 @@
+Class {
+	#name : #MonomorphizedDataDeclTest,
+	#superclass : #TestCaseWithZ3Context,
+	#instVars : [
+		'listType'
+	],
+	#category : #'Z3-Tests-ADT'
+}
+
+{ #category : #running }
+MonomorphizedDataDeclTest >> emptiness [
+	"Emptiness is the characteristic function of empty lists:
+	 it is 1 if the given argument is empty,
+	 0 if the given argument is non-empty."
+	| l emptiness ite |
+	l := listType mkConst: 'l'.
+	emptiness := 'emptiness' recursiveFunctionFrom: {listType} to: Int sort.
+	ite := ((listType recognizerFor: 'nil') value: l) ifTrue: [1 toInt] ifFalse: [0 toInt].
+	emptiness value: l is: ite.
+	^emptiness
+]
+
+{ #category : #running }
+MonomorphizedDataDeclTest >> len [
+	| len l |
+	l := listType mkConst: 'l'.
+	len := 'len' recursiveFunctionFrom: {listType} to: Int sort.
+	len value: l is: (((listType recognizerFor: 'nil') value: l)
+		ifTrue: [0 toInt]
+		ifFalse: [ (len value: ((listType accessorNamed: 'cdr') value: l)) + 1 ]).
+	^len
+]
+
+{ #category : #running }
+MonomorphizedDataDeclTest >> setUp [
+	listType := MonomorphizedDataDecl named: 'List'.
+	listType declare: 'cons' accessors: { 'car'->Int sort. 'cdr'->listType }.
+	listType declare: 'nil' accessors: #().
+	listType := listType create
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testAllNilsAreEqual [
+	| nilConstructor nil1 nil2 |
+	nil1 := (listType constructorNamed: 'nil') value.
+	self assert: nil1 sort equals: listType.
+	nil2 := (listType constructorNamed: 'nil') value.
+
+	self assert: nil2 sort equals: listType.
+	self assert: (nil1 === nil2) isValid
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testListCreation [
+	| l ll |
+	l := listType mkConst: 'l'.
+	ll := listType mkConst: 'll'.
+
+	self assert: l  sort  equals: listType.
+	self assert: ll sort  equals: listType
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testMeasure [
+	| l ite emptiness |
+	Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ].
+
+	l := listType mkConst: 'll'.
+	self assert: (
+		"The only list whose length is 0, is Nil."
+		Z3Solver isValid: (self emptiness value: l) > 0 ==> ((listType recognizerFor: 'nil') value: l)
+	)
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testNilHasLength0 [
+	| nil1 |
+	Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ].
+
+	nil1 := (listType constructorNamed: 'nil') value.
+	self
+		assert: self len ∘ nil1
+		equals: 0
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testNotAllListsEqual [
+	| l ll |
+	l := listType mkConst: 'l'.
+	ll := listType mkConst: 'll'.
+	self deny: (l === ll) isValid
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testNumConstructors [
+	self assert: listType numConstructors equals: 2
+]
+
+{ #category : #tests }
+MonomorphizedDataDeclTest >> testSingletonLengthIs1 [
+	| singleton |
+	Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ].
+
+	singleton := (listType constructorNamed: 'cons')
+		value: 'head' toInt
+		value: (listType constructorNamed: 'nil') value.
+	self assert: (self len ∘ singleton === 1) isValid
+]

src/Z3/MonomorphizedDataDecl.class.st

@@ -0,0 +1,110 @@
+"
+I provide a level of API to Z3 Datatypes slightly higher than the C API.
+My structure is similar to the Python Z3Datatype, but I dont attempt to
+""be dynamic"".  I am intended to bridge between Z3DatatypeSort (which
+follows the C API) and DataDecl in Fixpoint.  Clients should preferably
+NOT use this intermediate-level API.
+"
+Class {
+	#name : #MonomorphizedDataDecl,
+	#superclass : #Object,
+	#instVars : [
+		'name',
+		'constructors'
+	],
+	#category : #'Z3-Core'
+}
+
+{ #category : #'SMT interface' }
+MonomorphizedDataDecl class >> createDatatypes: ds [
+	| clists constructors z3sorts |
+	constructors := OrderedCollection new.
+	clists := OrderedCollection new.
+	clists := ds collect: [ :d |
+		| cs clist |
+		cs := d constructors collect: [ :c |
+			| cname rname fs fsrs  fnames sorts refs |
+			cname := c first toZ3Symbol.
+			rname := c second toZ3Symbol.
+			fs := c last.
+			fsrs := fs collect: [ :f |
+				| fname ftype |
+				fname := f key.
+				ftype := f value.
+				{fname toZ3Symbol}, (ftype sort_index: ds) ].
+			fsrs := fsrs unzip: 3.
+			fnames := fsrs first. sorts := fsrs second. refs := fsrs third.
+			constructors add: (Z3Constructor
+				name: cname
+				recognizer: rname
+				fields: (fnames zip: sorts)
+				referencing: refs) "and this returns the constructor from the block"
+			].
+		clist := Z3ConstructorList withAll: cs.
+		clists add: clist
+	].
+	z3sorts := Z3DatatypeSort names: (ds collect: #name) constructorLists: clists.
+	clists do: #delete.
+	constructors do: #delete.
+	^z3sorts
+]
+
+{ #category : #'instance creation' }
+MonomorphizedDataDecl class >> named: aString [
+	^self basicNew
+		name: aString;
+		constructors: OrderedCollection new;
+		yourself
+]
+
+{ #category : #accessing }
+MonomorphizedDataDecl >> constructors [
+	^ constructors
+]
+
+{ #category : #accessing }
+MonomorphizedDataDecl >> constructors: anObject [
+	constructors := anObject
+]
+
+{ #category : #'SMT interface' }
+MonomorphizedDataDecl >> create [
+	"Create a Z3 datatype based on the constructors declared via #declare:.                                    
+	 This is a convenience wrapper around #createDatatypes:.
+	 The latter must be used to define mutually recursive datatypes."
+	^(self class createDatatypes: {self}) first
+]
+
+{ #category : #'SMT interface' }
+MonomorphizedDataDecl >> declare: constructorName accessors: assocs [ 
+	self
+		declareCore: constructorName recognizer: 'Doesnt_work_anyway_', constructorName
+		accessors: assocs
+]
+
+{ #category : #'SMT interface' }
+MonomorphizedDataDecl >> declareCore: constructorName recognizer: rec_name accessors: assocs [ 
+	constructors addLast: { constructorName . rec_name . assocs }
+]
+
+{ #category : #accessing }
+MonomorphizedDataDecl >> name [
+	^ name
+]
+
+{ #category : #accessing }
+MonomorphizedDataDecl >> name: anObject [
+	name := anObject
+]
+
+{ #category : #printing }
+MonomorphizedDataDecl >> printOn: aStream [
+	aStream nextPutAll: 'Datatype '.
+	aStream nextPutAll: self name
+]
+
+{ #category : #'recursive adt' }
+MonomorphizedDataDecl >> sort_index: knownDatatypes [
+	(knownDatatypes occurrencesOf: self) = 1 ifFalse: [ self error: 'One and only one occurrence of each datatype is expected' ].
+	^{nil . (knownDatatypes indexOf: self) - 1}
+]

src/Z3/Z3Sort.class.st

@@ -169,3 +169,8 @@ Z3Sort >> numeralFrom: aString [
 Z3Sort >> raisedTo: B [
 	^B ==> self
 ]
+
+{ #category : #'recursive adt' }
+Z3Sort >> sort_index: _ [ 
+	^{self . 0}
+]