Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor datatypes #338

Closed
wants to merge 6 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions src/Z3-Tests/Z3TreeDatatypeTest.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ Z3TreeDatatypeTest >> testAlwaysSomething [
| u isNil isCons |
"is_nil(u) or is_cons(u)"
u := cell mkConst: 'u'.
isNil := cell is_nil: u.
isCons := cell is_cons: u.
isNil := u is: cell nil.
isCons := u is: cell cons.
self assert: (Z3Solver isValid: isNil | isCons)
]

Expand All @@ -50,16 +50,16 @@ Z3TreeDatatypeTest >> testDestructors [
u := cell mkConst: 'u'.
fml1 := u === (cell cons: (cell car: u) _: (cell cdr: u)).
self deny: (Z3Solver isValid: fml1). "by itself, fml1 does not always hold"
fml := (cell is_cons: u) ==> fml1.
fml := (u is: cell cons) ==> fml1.
self assert: (Z3Solver isValid: fml). "but for cells that are cons cells, it's valid"
]

{ #category : #tests }
Z3TreeDatatypeTest >> testNilNotCons [
"nil != cons(nil, nil)"
| nilCell l1 |
nilCell := cell nil.
l1 := consCon value: nilCell value: nilCell.
nilCell := cell nil new.
l1 := cell cons with: nilCell with: nilCell.
self assert: (Z3Solver isValid: (nilCell===l1) not).

]
Expand Down
8 changes: 8 additions & 0 deletions src/Z3/Datatype.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,14 @@ Datatype >> doesNotUnderstand: aMessage [
^fn value: self
]

{ #category : #testing }
Datatype >> is: datatypeComponent [
self sort == datatypeComponent sort ifTrue:[
^datatypeComponent recognizer value: self
] ifFalse:[
^Bool false.
]
]
{ #category : #converting }
Datatype >> toDatatype: aZ3Sort [
self sort == aZ3Sort ifFalse: [ ^self error: 'Cannot coerce' ].
Expand Down
5 changes: 5 additions & 0 deletions src/Z3/Object.extension.st
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,11 @@ Object >> toBool [
self error: 'No automatic coerction to Bool, please coerce manually'
]

{ #category : #'*Z3' }
Object >> toDatatype: datatypeSort [
self error: 'No automatic coerction to Datatype, please coerce manually'
]

{ #category : #'*Z3' }
Object >> toInt [
self error: 'No automatic coerction to Int, please coerce manually'
Expand Down
109 changes: 52 additions & 57 deletions src/Z3/Z3Datatype.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -3,75 +3,80 @@ Class {
#superclass : #Object,
#instVars : [
'name',
'ctx',
'constructors'
],
#category : #'Z3-Core'
}

{ #category : #'as yet unclassified' }
Z3Datatype class >> createDatatypes: ds [
| num out clists toDelete drefs |
Z3Datatype class >> createDatatypes: datatypes [
| num datatypeSorts ctorLists toDelete drefs |
toDelete := OrderedCollection new.
num := ds size.
clists := ds collect: [ :d |
| cs clist |
cs := d constructors collect: [ :c |
| cname rname fs fsrs fnames sorts refs z3c |
cname := c first toZ3Symbol.
rname := c second toZ3Symbol.
fs := c last.
fsrs := fs collect: [ :f |
num := datatypes size.
ctorLists := datatypes collect: [ :d |
| ctors ctorList |
ctors := d constructors collect: [ :c |
| ctorName recognizerName ctorFields fsrs ctorFieldNames ctorFieldSorts ctorFieldSortRefs ctor |
ctorName := c first toZ3Symbol.
recognizerName := c second toZ3Symbol.
ctorFields := c last.
fsrs := ctorFields collect: [ :f |
| fname ftype |
fname := f key.
ftype := f value.
{fname toZ3Symbol}, (ftype sort_reft: ds) ].
{fname toZ3Symbol}, (ftype sort_reft: datatypes) ].
fsrs := fsrs unzip: 3.
fnames := fsrs first. sorts := fsrs second. refs := fsrs third.
z3c := Z3 mk_constructor: Z3Context current
_: cname
_: rname
_: fs size
_: fnames
_: sorts
_: refs.
ctorFieldNames := fsrs first. ctorFieldSorts := fsrs second. ctorFieldSortRefs := fsrs third.
ctor := Z3 mk_constructor: Z3Context current
_: ctorName
_: recognizerName
_: ctorFields size
_: ctorFieldNames
_: ctorFieldSorts
_: ctorFieldSortRefs.
"TODO: to_delete.append(ScopedConstructor(cs[j], ctx))"
z3c ].
clist := Z3 mk_constructor_list: Z3Context current
_: cs size
_: cs.
ctor ].
ctorList := Z3 mk_constructor_list: Z3Context current
_: ctors size
_: ctors.
"to_delete.append(ScopedConstructorList(clists[i], ctx))"
clist ].
out := Array new: num.
ctorList ].
datatypeSorts := Array new: num.
Z3 mk_datatypes: Z3Context current
_: num
_: ((ds collect: #name) collect: #toZ3Symbol)
_: out
_: clists.
_: ((datatypes collect: #name) collect: #toZ3Symbol)
_: datatypeSorts
_: ctorLists.

drefs:= out collect: [ :dref |
(1 to: dref numConstructors) do: [ :j |
| cref cref_name cref_arity rref |
cref := dref constructor: j-1.
cref_name := cref name.
cref_arity := cref arity.
"cref_arity = 0 ifTrue: [ cref := cref value ]."
dref at: cref_name put: cref.
rref := dref recognizer: j-1.
dref at: 'is_', cref_name put: rref.
1 to: cref_arity do: [ :k |
| aref |
aref := dref accessor: j-1 idx: k-1.
dref at: aref name put: aref ] ].
dref ].
^drefs
datatypeSorts do: [ :datatypeSort |
(0 to: datatypeSort numConstructors - 1) do: [ :ctorIndex |
| ctorFunc ctorName ctorArity recognizerFunc accessorFuncs datatypeComponent |
ctorFunc := datatypeSort constructor: ctorIndex.
ctorName := ctorFunc name.
ctorArity := ctorFunc arity.
recognizerFunc := datatypeSort recognizer: ctorIndex.
accessorFuncs :=
(0 to: ctorArity - 1) collect:
[:accessorIndex | datatypeSort accessor: ctorIndex idx: accessorIndex ].

"New style, create 'component'"
datatypeComponent := Z3DatatypeComponent new.
datatypeComponent constructor: ctorFunc; recognizer: recognizerFunc; accessors: accessorFuncs.
datatypeSort components at: datatypeComponent name put: datatypeComponent.

"Old style kept for compatibility"
datatypeSort at: ctorName put: ctorFunc.
datatypeSort at: 'is_', ctorName put: recognizerFunc.
accessorFuncs do: [:accessorFunc | datatypeSort at: accessorFunc name put: accessorFunc ]
].
].
^datatypeSorts

]

{ #category : #'instance creation' }
Z3Datatype class >> named: aString [
^self basicNew
ctx: Z3Context current;
name: aString;
constructors: OrderedCollection new;
yourself
Expand All @@ -94,16 +99,6 @@ Z3Datatype >> create [
^(Z3Datatype createDatatypes: {self}) first
]

{ #category : #accessing }
Z3Datatype >> ctx [
^ ctx
]

{ #category : #accessing }
Z3Datatype >> ctx: anObject [
ctx := anObject
]

{ #category : #'as yet unclassified' }
Z3Datatype >> declare: constructorName [
self declare: constructorName accessors: #()
Expand Down
103 changes: 103 additions & 0 deletions src/Z3/Z3DatatypeComponent.class.st
Original file line number Diff line number Diff line change
@@ -0,0 +1,103 @@
Class {
#name : #Z3DatatypeComponent,
#superclass : #Object,
#instVars : [
'constructor',
'recognizer',
'accessors'
],
#category : #'Z3-Core'
}

{ #category : #private }
Z3DatatypeComponent >> accessors [
^ accessors
]

{ #category : #private }
Z3DatatypeComponent >> accessors: aCollection [
accessors := aCollection
]

{ #category : #private }
Z3DatatypeComponent >> constructor [
^ constructor
]

{ #category : #private }
Z3DatatypeComponent >> constructor: anObject [
constructor := anObject
]

{ #category : #private }
Z3DatatypeComponent >> name [
^constructor name
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> new [
^self withValues: #()
]

{ #category : #private }
Z3DatatypeComponent >> recognizer [
^ recognizer
]

{ #category : #private }
Z3DatatypeComponent >> recognizer: anObject [
recognizer := anObject
]

{ #category : #private }
Z3DatatypeComponent >> sort [
^constructor range
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 [
^self withValues: { a1 }
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 [
^self withValues: { a1 . a2 }
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 [
^self withValues: { a1 . a2 . a3}
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 with: a4 [
^self withValues: { a1 . a2 . a3 . a4}
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 with: a4 with: a5 [
^self withValues: { a1 . a2 . a3 . a4 . a5}
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 with: a4 with: a5 with: a6 [
^self withValues: { a1 . a2 . a3 . a4 . a5 .a6 }
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 with: a4 with: a5 with: a6 with: a7 [
^self withValues: { a1 . a2 . a3 . a4 . a5 . a6 . a7}
]

{ #category : #'instance creation' }
Z3DatatypeComponent >> with: a1 with: a2 with: a3 with: a4 with: a5 with: a6 with: a7 with: a8 [
^self withValues: { a1 . a2 . a3 . a4 . a5 . a6 . a7 . a8 }
]

{ #category : #private }
Z3DatatypeComponent >> withValues: values [
constructor arity ~~ values size ifTrue:[
self error: 'Invalid number of arguments'
].
^constructor valueWithArguments: values
]
38 changes: 26 additions & 12 deletions src/Z3/Z3DatatypeSort.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@ Class {
#name : #Z3DatatypeSort,
#superclass : #Z3Sort,
#instVars : [
'attrs'
'attrs',
'components'
],
#category : #'Z3-Core'
}
Expand All @@ -28,6 +29,11 @@ Z3DatatypeSort >> cast: val [
^val toDatatype: self
]

{ #category : #private }
Z3DatatypeSort >> components [
^ components
]

{ #category : #'F-Algebra' }
Z3DatatypeSort >> constructor: idx [
"Answer a constructor of the datatype self.
Expand All @@ -36,19 +42,27 @@ Z3DatatypeSort >> constructor: idx [
^ Z3 get_datatype_sort_constructor: ctx _: self _: idx
]

{ #category : #'F-Algebra' }
Z3DatatypeSort >> constructors [
^(1 to: self numConstructors) collect: [ :i | self constructor: i-1 ]
]

{ #category : #'function application' }
Z3DatatypeSort >> doesNotUnderstand: aMessage [
| z3name fn convertedArgs |
aMessage selector isBinary ifTrue: [ ^self shouldBeImplemented ].
z3name := aMessage selector z3likeSelector.
fn := self attrs at: z3name ifAbsent: [ ^super doesNotUnderstand: aMessage ].
convertedArgs := fn domain collectWithIndex: [ :argSort :j | argSort cast: (aMessage arguments at: j) ].
^fn valueWithArguments: convertedArgs
| component z3name fn convertedArgs |

component := components at: aMessage selector ifAbsent:[
"Old code, will wanish"
aMessage selector isBinary ifTrue: [ ^self shouldBeImplemented ].
z3name := aMessage selector z3likeSelector.
fn := self attrs at: z3name ifAbsent: [ ^super doesNotUnderstand: aMessage ].
convertedArgs := fn domain collectWithIndex: [ :argSort :j | argSort cast: (aMessage arguments at: j) ].
^fn valueWithArguments: convertedArgs
].
^ component
]

{ #category : #initialization }
Z3DatatypeSort >> initializeWithAddress: anExternalAddress context: aZ3Context [
super initializeWithAddress: anExternalAddress context: aZ3Context.
components := SmallDictionary new.


]

{ #category : #'type theory' }
Expand Down
Loading