From a2e65ed8ab81a2dd513c8f3416595408f87b9aa3 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Sat, 16 Nov 2024 16:56:51 -0500
Subject: [PATCH] [MathNotaiton] Decode unsafe names of Z3Sorts

---
 .../UnsafeZ3NameTest.class.st                 | 54 +++++++++++++++++++
 src/MathNotation/Z3BoolSort.extension.st      |  5 ++
 src/MathNotation/Z3DatatypeSort.extension.st  | 11 ++++
 src/MathNotation/Z3IntSort.extension.st       |  5 ++
 src/MathNotation/Z3RealSort.extension.st      | 11 ++++
 .../Z3UninterpretedSort.extension.st          | 11 ++++
 src/Z3/Z3RealSort.class.st                    |  5 --
 7 files changed, 97 insertions(+), 5 deletions(-)
 create mode 100644 src/MathNotation-Tests/UnsafeZ3NameTest.class.st
 create mode 100644 src/MathNotation/Z3DatatypeSort.extension.st
 create mode 100644 src/MathNotation/Z3RealSort.extension.st
 create mode 100644 src/MathNotation/Z3UninterpretedSort.extension.st

diff --git a/src/MathNotation-Tests/UnsafeZ3NameTest.class.st b/src/MathNotation-Tests/UnsafeZ3NameTest.class.st
new file mode 100644
index 000000000..4feafe663
--- /dev/null
+++ b/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: 'ℤ'
+	
+]
diff --git a/src/MathNotation/Z3BoolSort.extension.st b/src/MathNotation/Z3BoolSort.extension.st
index f53895f29..484a95793 100644
--- a/src/MathNotation/Z3BoolSort.extension.st
+++ b/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)
 ]
diff --git a/src/MathNotation/Z3DatatypeSort.extension.st b/src/MathNotation/Z3DatatypeSort.extension.st
new file mode 100644
index 000000000..fb3a22add
--- /dev/null
+++ b/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
+]
diff --git a/src/MathNotation/Z3IntSort.extension.st b/src/MathNotation/Z3IntSort.extension.st
index 5e6bd3b95..49d31bf31 100644
--- a/src/MathNotation/Z3IntSort.extension.st
+++ b/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
 ]
diff --git a/src/MathNotation/Z3RealSort.extension.st b/src/MathNotation/Z3RealSort.extension.st
new file mode 100644
index 000000000..fa27f88f9
--- /dev/null
+++ b/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
+]
diff --git a/src/MathNotation/Z3UninterpretedSort.extension.st b/src/MathNotation/Z3UninterpretedSort.extension.st
new file mode 100644
index 000000000..82268e192
--- /dev/null
+++ b/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
+]
diff --git a/src/Z3/Z3RealSort.class.st b/src/Z3/Z3RealSort.class.st
index ffd848a25..85d724400 100644
--- a/src/Z3/Z3RealSort.class.st
+++ b/src/Z3/Z3RealSort.class.st
@@ -14,8 +14,3 @@ Z3RealSort >> nodeClass [
 	^ Real
 
 ]
-
-{ #category : #printing }
-Z3RealSort >> printString [
-	^String with: Character reals
-]