[Z3] Initial support for Z3 Strings (v2)

src/Z3-Tests/SimpleZ3Test.class.st

@@ -238,6 +238,15 @@ SimpleZ3Test >> testCreateArray [
 	self assert: a astToString equals: '(Array Int Bool)'
 ]
 
+{ #category : #tests }
+SimpleZ3Test >> testCreateString [
+	| s |
+	s := 'abc' toZ3String.
+	self assert: s sort isStringSort.
+	self assert: s isZ3String.
+	self assert: s getString = 'abc'
+]
+
 { #category : #tests }
 SimpleZ3Test >> testEmptySymbolHasNullPointer [
 	| emptySymbol |

src/Z3/Object.extension.st

@@ -101,6 +101,11 @@ Object >> isReal [
 	^false
 ]
 
+{ #category : #'*Z3' }
+Object >> isZ3String [
+	^ false
+]
+
 { #category : #'*Z3' }
 Object >> isZ3Symbol [
 	^ false
@@ -126,6 +131,11 @@ Object >> toReal [
 	self error: 'No automatic coerction to Real, please coerce manually'
 ]
 
+{ #category : #'*Z3' }
+Object >> toZ3String [
+	self error: 'No automatic coerction to Z3String, please coerce manually'
+]
+
 { #category : #'*Z3' }
 Object >> toZ3Symbol [
 	^Z3Symbol from: self

src/Z3/String.extension.st

@@ -57,3 +57,8 @@ String >> toSort [
 String >> toZ3Sort: s [
 	^s mkConst: self
 ]
+
+{ #category : #'*Z3' }
+String >> toZ3String [
+	^Z3String mkString: self
+]

src/Z3/Z3AST.class.st

@@ -172,6 +172,11 @@ Z3AST >> isSymbolic [
 	^self simplify isNumeral not
 ]
 
+{ #category : #testing }
+Z3AST >> isZ3String [
+	^ Z3 is_string: ctx _: self
+]
+
 { #category : #accessing }
 Z3AST >> kind [
 	^ self subclassResponsibility

src/Z3/Z3Context.class.st

@@ -321,6 +321,16 @@ Z3Context >> mkSolverForLogic: logic [
 	^ Z3 mk_solver_for_logic: self _: (self mkSymbol: logic)
 ]
 
+{ #category : #'API wrappers' }
+Z3Context >> mkString: aString [ 
+	^Z3 mk_string: self _: aString
+]
+
+{ #category : #'API wrappers' }
+Z3Context >> mkStringSort [
+	^Z3 mk_string_sort: self
+]
+
 { #category : #'API wrappers' }
 Z3Context >> mkSymbol [
 	"The empty symbol (a special symbol in Z3).

src/Z3/Z3Sort.class.st

@@ -28,6 +28,7 @@ Z3Sort class >> classForSortKind: sortKind [
 	sortKind = BV_SORT ifTrue: [ ^ Z3BitVectorSort ].
 	sortKind = ARRAY_SORT ifTrue: [ ^ Z3ArraySort ].
 	sortKind = DATATYPE_SORT ifTrue: [ ^ Z3DatatypeSort ].
+	sortKind = SEQ_SORT ifTrue: [ ^ Z3StringSort ].
 
 	self error: '(Yet) unsupported sort kind: ' , sortKind printString             
 
@@ -57,6 +58,11 @@ Z3Sort class >> real [
 	^ Z3Context current mkRealSort
 ]
 
+{ #category : #'instance creation' }
+Z3Sort class >> string [
+	^ Z3Context current mkStringSort
+]
+
 { #category : #'instance creation' }
 Z3Sort class >> uninterpretedSortNamed: aName [
 	^(Z3Symbol from: aName) mkUninterpretedSort
@@ -104,6 +110,13 @@ Z3Sort >> isIntSort [
 	^ false
 ]
 
+{ #category : #testing }
+Z3Sort >> isStringSort [
+	"In this case, we call the dedicated Z3 API,
+	 as opposed to isIntSort etc which have no such API."
+	^ Z3 is_string_sort: ctx _: self
+]
+
 { #category : #accessing }
 Z3Sort >> kind [
 	^ SORT_AST

src/Z3/Z3String.class.st

@@ -0,0 +1,32 @@
+Class {
+	#name : #Z3String,
+	#superclass : #Z3Node,
+	#category : #'Z3-Core'
+}
+
+{ #category : #'instance creation' }
+Z3String class >> mkString: aString [ 
+	^Z3Context current mkString: aString
+]
+
+{ #category : #types }
+Z3String class >> sort [
+	^Z3Sort string
+]
+
+{ #category : #converting }
+Z3String >> asString [
+	^ self getString
+]
+
+{ #category : #API }
+Z3String >> getString [
+	"Caveat programmator:
+	 We do not begin to address the escaping issues in https://github.com/Z3Prover/z3/issues/2286"
+	^Z3 get_string: ctx _: self
+]
+
+{ #category : #converting }
+Z3String >> toZ3String [
+	^self
+]

src/Z3/Z3StringSort.class.st

@@ -0,0 +1,15 @@
+Class {
+	#name : #Z3StringSort,
+	#superclass : #Z3Sort,
+	#category : #'Z3-Core'
+}
+
+{ #category : #'type theory' }
+Z3StringSort >> cast: value [
+	^ value toZ3String
+]
+
+{ #category : #'type theory' }
+Z3StringSort >> nodeClass [
+	^Z3String
+]