Implement proof-of-concept FTC/FObj-to-Data bridge

shingarov · Oct 29, 2024 · b56bfb8 · b56bfb8
1 parent fd376e9
commit b56bfb8
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 19 deletions.
diff --git a/src/Refinements/FTC.class.st b/src/Refinements/FTC.class.st
@@ -42,16 +42,21 @@ FTC >> containsFVar [
 
 { #category : #hotel }
 FTC >> fappSmtSort: ts originalFApp: anFApp in: γ [
-	| j |
 	self isSetCon ifTrue: [
 		ts size = 1 ifFalse: [ self error ].
 		^(ts first z3sort: γ) mkSetSort
 	].
 	self isMapCon ifTrue: [ self shouldBeImplemented ].
 	self isBitVec ifTrue: [ self shouldBeImplemented ].
 
-	j := PreSort hotel addElement: anFApp.
-	^Z3Sort uninterpretedSortNamed: j
+	^(self maybeDataIn: γ)
+		ifNil: [ | j |
+			j := PreSort hotel addElement: anFApp.
+			Z3Sort uninterpretedSortNamed: j
+		] ifNotNil: [ :d |
+			d ddVars = ts size ifFalse: [ self error ].
+			d instantiateZ3Sort: (ts collect: [ :t | t z3sort: γ ])
+		]
 ]
 
 { #category : #comparing }
@@ -83,13 +88,25 @@ Cf. fappSmtSort in Theories.hs
 	^typeConstructor symbol = 'Set_Set'
 ]
 
+{ #category : #hotel }
+FTC >> maybeDataIn: aSymEnv [
+	^aSymEnv data
+		at: typeConstructor symbol
+		ifAbsent: [ nil ]
+]
+
 { #category : #printing }
 FTC >> printOn: aStream [
 	aStream nextPutAll: 'FTC ('.
 	typeConstructor printOn: aStream.
 	aStream nextPutAll: ')'.
 ]
 
+{ #category : #hotel }
+FTC >> smt2sort: γ [
+	^self fappSmtSort: #() originalFApp: self in: γ
+]
+
 { #category : #substitution }
 FTC >> sortSubst: θ [
 "TODO: investigate.
@@ -112,11 +129,3 @@ FTC >> typeConstructor [
 FTC >> typeConstructor: anObject [
 	typeConstructor := anObject
 ]
-
-{ #category : #hotel }
-FTC >> z3sort: _ [
-	| h j |
-	h := PreSort hotel.
-	j := h addElement: self.
-	^Z3Sort uninterpretedSortNamed: j
-]
diff --git a/src/Refinements/Z3Sort.extension.st b/src/Refinements/Z3Sort.extension.st
@@ -32,14 +32,6 @@ Z3Sort >> falseRefinement [
 	^self | [ :x | Bool false ]
 ]
 
-{ #category : #'*Refinements' }
-Z3Sort >> fappSmtSort: ts originalFApp: anFApp in: _ [
-	| j |
-self error: 'this method will be removed, this is replaced by FObj>>fappSmtSort'.
-	j := PreSort hotel addElement: anFApp.
-	^Z3Sort uninterpretedSortNamed: j
-]
-
 { #category : #'*Refinements' }
 Z3Sort >> goFunctionSort: vs _: ss [ 
 	^{ vs reversed . ss reversed . self }