Implement beginnigs of Z3 interface for DataDecl

NB: Still no datatype recursion!!! See e.g. Horn L5cons00data.
shingarov · Oct 29, 2024 · fd376e9 · fd376e9
1 parent b7d5d77
commit fd376e9
Show file tree

Hide file tree

Showing 3 changed files with 33 additions and 0 deletions.
diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st
@@ -55,6 +55,17 @@ DataCtor >> printOn: aStream [
 		nextPutAll: ')'
 ]
 
+{ #category : #'SMT interface' }
+DataCtor >> smt2ctor: ts [
+	| instantiatedFields |
+	instantiatedFields := dcFields collect: [ :field | field dfName -> (field smt2field: ts) ].
+	^Z3Constructor
+		name: self symbol
+		recognizer: 'is-', self symbol
+		fields: instantiatedFields
+		referencing: (Array new: dcFields size withAll: 0)  "BOGUS, implement mutually-recursive ADTs!"	
+]
+
 { #category : #Symbolic }
 DataCtor >> symbol [
 	^dcName

diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st
@@ -69,12 +69,26 @@ DataDecl >> gtInspectorConstructorsIn: composite [
 		display: [ ddCtors ]
 ]
 
+{ #category : #'SMT interface' }
+DataDecl >> instantiateZ3Sort: ts [
+	| ctors z3datatypeSort |
+	ctors := self smt2datactors: ts.
+	z3datatypeSort := Z3DatatypeSort name: self symbol  constructors: ctors.
+	ctors do: #delete.
+	^z3datatypeSort
+]
+
 { #category : #printing }
 DataDecl >> printOn: aStream [
 	aStream nextPutAll: 'data '.
 	aStream nextPutAll: self ddTyCon symbol
 ]
 
+{ #category : #'SMT interface' }
+DataDecl >> smt2datactors: ts [
+	^ddCtors collect: [ :ctor | ctor smt2ctor: ts ]
+]
+
 { #category : #Symbolic }
 DataDecl >> symbol [
 "

diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st
@@ -43,3 +43,11 @@ DataField >> dfSort [
 DataField >> dfSort: anObject [
 	dfSort := anObject
 ]
+
+{ #category : #'SMT interface' }
+DataField >> smt2field: ts [
+	| θ monomorphicSort |
+	θ := Dictionary newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]).
+	monomorphicSort := dfSort apply: θ.
+	^monomorphicSort "z3sort"
+]