[MathNotaiton] Decode unsafe names of Z3Sorts

src/MathNotation-Tests/UnsafeZ3NameTest.class.st

@@ -0,0 +1,54 @@
+Class {
+	#name : #UnsafeZ3NameTest,
+	#superclass : #TestCaseWithZ3Context,
+	#category : #'MathNotation-Tests'
+}
+
+{ #category : #tests }
+UnsafeZ3NameTest >> testIntName [
+	| Z |
+	Z := Int sort.
+	self assert: Z name isZ3Symbol.
+	self assert: Z name isStringSymbol.
+	self deny:   Z name isIntSymbol.
+	self assert: Z name getString equals: 'Int' "NB: NOT 'ℤ'!!!"
+
+]
+
+{ #category : #tests }
+UnsafeZ3NameTest >> testUnsafeEnum [
+	| fruit consts testers |
+	consts  := Cell new.
+	testers := Cell new.
+	fruit := Z3DatatypeSort
+		mkEnumerationSort: 'rotten#fruit' encodeUnsafe
+		elements: { 'apple'. 'banana'. 'orange' }
+		consts: consts
+		testers: testers.
+	self assert: fruit name isZ3Symbol.
+	self assert: fruit name isStringSymbol.
+	self deny:   fruit name isIntSymbol.
+	self assert: fruit name getString equals: 'rottenß35ßfruit'.
+	self assert: fruit unsafeName equals: 'rotten#fruit'
+
+]
+
+{ #category : #tests }
+UnsafeZ3NameTest >> testUnsafeUninterpreted [
+	| s |
+	s := Z3Sort uninterpretedSortNamed: '(a b)' encodeUnsafe.
+	self assert: s name isZ3Symbol.
+	self assert: s name isStringSymbol.
+	self deny:   s name isIntSymbol.
+	self assert: s name getString equals: 'ß40ßaß32ßbß41ß'.
+	self assert: s unsafeName equals: '(a b)'
+
+]
+
+{ #category : #tests }
+UnsafeZ3NameTest >> testZahlenForInt [
+	| Z |
+	Z := Int sort.
+	self assert: Z unsafeName equals: 'ℤ'
+
+]

src/MathNotation/Z3BoolSort.extension.st

@@ -2,5 +2,10 @@ Extension { #name : #Z3BoolSort }
 
 { #category : #'*MathNotation' }
 Z3BoolSort >> printString [
+	^self unsafeName
+]
+
+{ #category : #'*MathNotation' }
+Z3BoolSort >> unsafeName [
 	^String with: (Character codePoint: 16r1D539)
 ]

src/MathNotation/Z3DatatypeSort.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #Z3DatatypeSort }
+
+{ #category : #'*MathNotation' }
+Z3DatatypeSort >> printString [
+	^self unsafeName
+]
+
+{ #category : #'*MathNotation' }
+Z3DatatypeSort >> unsafeName [
+	^self name getString decodeUnsafe
+]

src/MathNotation/Z3IntSort.extension.st

@@ -2,5 +2,10 @@ Extension { #name : #Z3IntSort }
 
 { #category : #'*MathNotation' }
 Z3IntSort >> printString [
+	^self unsafeName
+]
+
+{ #category : #'*MathNotation' }
+Z3IntSort >> unsafeName [
 	^String with: Character zahlen
 ]

src/MathNotation/Z3RealSort.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #Z3RealSort }
+
+{ #category : #'*MathNotation' }
+Z3RealSort >> printString [
+	^self unsafeName
+]
+
+{ #category : #'*MathNotation' }
+Z3RealSort >> unsafeName [
+	^String with: Character reals
+]

src/MathNotation/Z3UninterpretedSort.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #Z3UninterpretedSort }
+
+{ #category : #'*MathNotation' }
+Z3UninterpretedSort >> printOn: aStream [
+	aStream nextPutAll: self unsafeName
+]
+
+{ #category : #'*MathNotation' }
+Z3UninterpretedSort >> unsafeName [
+	^self name asString decodeUnsafe
+]

src/Z3/Z3RealSort.class.st

@@ -14,8 +14,3 @@ Z3RealSort >> nodeClass [
 	^ Real
 
 ]
-
-{ #category : #printing }
-Z3RealSort >> printString [
-	^String with: Character reals
-]