BEGINNING IDIOTIC DOODLES

shingarov · Oct 13, 2024 · e42ed18 · e42ed18
1 parent a156555
commit e42ed18
Showing 1 changed file with 17 additions and 3 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 [
-	| 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 maybeData
+		ifNil: [
+			| j |
+			j := PreSort hotel addElement: anFApp.
+			^Z3Sort uninterpretedSortNamed: j
+		] ifNotNil: [
+			^self shouldBeImplemented
+		]
 ]
 
 { #category : #comparing }
@@ -83,6 +88,15 @@ Cf. fappSmtSort in Theories.hs
 	^typeConstructor symbol = 'Set_Set'
 ]
 
+{ #category : #'as yet unclassified' }
+FTC >> maybeData [
+	| γ |
+	γ := Context readState: #symbolEnv.
+	^γ data
+		at: typeConstructor symbol
+		ifAbsent: [ nil ]
+]
+
 { #category : #printing }
 FTC >> printOn: aStream [
 	aStream nextPutAll: 'FTC ('.