From b4c3d1bd8eb46ae5ed96b2ebff66f03fde68847c Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Sun, 3 Nov 2024 19:57:18 -0500 Subject: [PATCH] [Z3] (Re)introduce MonomorphizedDataDecl mid-level Datatype API PR#351 ("Overhaul Z3-level Datatype API") has removed PyZ3-style "dynamic attributes" of Z3 Datatypes in favor of a strictly-disciplined API 100% faithful to Nikolaj's C API and proposed to "jump up" to LH-like DataDecl for the next-higher level. This is all good; but it misses one numance, namely how Z3 implements SMTLIB's "declare-datatypes" via instantiate_datatype() in pdecl.cpp. When PR#351 removed "dynamic attributes", it also removed some good stuff, i.e. recursive-sort-indexing. This commit reintroduces MonomorphizedDataDecl: similar to Z3Datatype minus the "dynamic" aspect. --- .../MonomorphizedDataDeclTest.class.st | 108 +++++++++++++++++ src/Z3/MonomorphizedDataDecl.class.st | 110 ++++++++++++++++++ src/Z3/Z3Sort.class.st | 5 + 3 files changed, 223 insertions(+) create mode 100644 src/Z3-Tests/MonomorphizedDataDeclTest.class.st create mode 100644 src/Z3/MonomorphizedDataDecl.class.st diff --git a/src/Z3-Tests/MonomorphizedDataDeclTest.class.st b/src/Z3-Tests/MonomorphizedDataDeclTest.class.st new file mode 100644 index 000000000..b690c4126 --- /dev/null +++ b/src/Z3-Tests/MonomorphizedDataDeclTest.class.st @@ -0,0 +1,108 @@ +Class { + #name : #MonomorphizedDataDeclTest, + #superclass : #TestCaseWithZ3Context, + #instVars : [ + 'listType' + ], + #category : #'Z3-Tests-ADT' +} + +{ #category : #running } +MonomorphizedDataDeclTest >> emptiness [ + "Emptiness is the characteristic function of empty lists: + it is 1 if the given argument is empty, + 0 if the given argument is non-empty." + | l emptiness ite | + l := listType mkConst: 'l'. + emptiness := 'emptiness' recursiveFunctionFrom: {listType} to: Int sort. + ite := ((listType recognizerFor: 'nil') value: l) ifTrue: [1 toInt] ifFalse: [0 toInt]. + emptiness value: l is: ite. + ^emptiness +] + +{ #category : #running } +MonomorphizedDataDeclTest >> len [ + | len l | + l := listType mkConst: 'l'. + len := 'len' recursiveFunctionFrom: {listType} to: Int sort. + len value: l is: (((listType recognizerFor: 'nil') value: l) + ifTrue: [0 toInt] + ifFalse: [ (len value: ((listType accessorNamed: 'cdr') value: l)) + 1 ]). + ^len +] + +{ #category : #running } +MonomorphizedDataDeclTest >> setUp [ + listType := MonomorphizedDataDecl named: 'List'. + listType declare: 'cons' accessors: { 'car'->Int sort. 'cdr'->listType }. + listType declare: 'nil' accessors: #(). + listType := listType create +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testAllNilsAreEqual [ + | nilConstructor nil1 nil2 | + nil1 := (listType constructorNamed: 'nil') value. + self assert: nil1 sort equals: listType. + nil2 := (listType constructorNamed: 'nil') value. + + self assert: nil2 sort equals: listType. + self assert: (nil1 === nil2) isValid +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testListCreation [ + | l ll | + l := listType mkConst: 'l'. + ll := listType mkConst: 'll'. + + self assert: l sort equals: listType. + self assert: ll sort equals: listType +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testMeasure [ + | l ite emptiness | + Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ]. + + l := listType mkConst: 'll'. + self assert: ( + "The only list whose length is 0, is Nil." + Z3Solver isValid: (self emptiness value: l) > 0 ==> ((listType recognizerFor: 'nil') value: l) + ) +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testNilHasLength0 [ + | nil1 | + Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ]. + + nil1 := (listType constructorNamed: 'nil') value. + self + assert: self len ∘ nil1 + equals: 0 +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testNotAllListsEqual [ + | l ll | + l := listType mkConst: 'l'. + ll := listType mkConst: 'll'. + self deny: (l === ll) isValid +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testNumConstructors [ + self assert: listType numConstructors equals: 2 +] + +{ #category : #tests } +MonomorphizedDataDeclTest >> testSingletonLengthIs1 [ + | singleton | + Smalltalk isSmalltalkX ifTrue: [ self skip:'Not supported on Smalltalk/X because of lack of dynamic deoptimization' ]. + + singleton := (listType constructorNamed: 'cons') + value: 'head' toInt + value: (listType constructorNamed: 'nil') value. + self assert: (self len ∘ singleton === 1) isValid +] diff --git a/src/Z3/MonomorphizedDataDecl.class.st b/src/Z3/MonomorphizedDataDecl.class.st new file mode 100644 index 000000000..9696d4901 --- /dev/null +++ b/src/Z3/MonomorphizedDataDecl.class.st @@ -0,0 +1,110 @@ +" +I provide a level of API to Z3 Datatypes slightly higher than the C API. +My structure is similar to the Python Z3Datatype, but I dont attempt to +""be dynamic"". I am intended to bridge between Z3DatatypeSort (which +follows the C API) and DataDecl in Fixpoint. Clients should preferably +NOT use this intermediate-level API. +" +Class { + #name : #MonomorphizedDataDecl, + #superclass : #Object, + #instVars : [ + 'name', + 'constructors' + ], + #category : #'Z3-Core' +} + +{ #category : #'SMT interface' } +MonomorphizedDataDecl class >> createDatatypes: ds [ + | clists constructors z3sorts | + constructors := OrderedCollection new. + clists := OrderedCollection new. + clists := ds collect: [ :d | + | cs clist | + cs := d constructors collect: [ :c | + | cname rname fs fsrs fnames sorts refs | + cname := c first toZ3Symbol. + rname := c second toZ3Symbol. + fs := c last. + fsrs := fs collect: [ :f | + | fname ftype | + fname := f key. + ftype := f value. + {fname toZ3Symbol}, (ftype sort_index: ds) ]. + fsrs := fsrs unzip: 3. + fnames := fsrs first. sorts := fsrs second. refs := fsrs third. + constructors add: (Z3Constructor + name: cname + recognizer: rname + fields: (fnames zip: sorts) + referencing: refs) "and this returns the constructor from the block" + ]. + clist := Z3ConstructorList withAll: cs. + clists add: clist + ]. + z3sorts := Z3DatatypeSort names: (ds collect: #name) constructorLists: clists. + clists do: #delete. + constructors do: #delete. + ^z3sorts +] + +{ #category : #'instance creation' } +MonomorphizedDataDecl class >> named: aString [ + ^self basicNew + name: aString; + constructors: OrderedCollection new; + yourself +] + +{ #category : #accessing } +MonomorphizedDataDecl >> constructors [ + ^ constructors +] + +{ #category : #accessing } +MonomorphizedDataDecl >> constructors: anObject [ + constructors := anObject +] + +{ #category : #'SMT interface' } +MonomorphizedDataDecl >> create [ + "Create a Z3 datatype based on the constructors declared via #declare:. + This is a convenience wrapper around #createDatatypes:. + The latter must be used to define mutually recursive datatypes." + ^(self class createDatatypes: {self}) first +] + +{ #category : #'SMT interface' } +MonomorphizedDataDecl >> declare: constructorName accessors: assocs [ + self + declareCore: constructorName recognizer: 'Doesnt_work_anyway_', constructorName + accessors: assocs +] + +{ #category : #'SMT interface' } +MonomorphizedDataDecl >> declareCore: constructorName recognizer: rec_name accessors: assocs [ + constructors addLast: { constructorName . rec_name . assocs } +] + +{ #category : #accessing } +MonomorphizedDataDecl >> name [ + ^ name +] + +{ #category : #accessing } +MonomorphizedDataDecl >> name: anObject [ + name := anObject +] + +{ #category : #printing } +MonomorphizedDataDecl >> printOn: aStream [ + aStream nextPutAll: 'Datatype '. + aStream nextPutAll: self name +] + +{ #category : #'recursive adt' } +MonomorphizedDataDecl >> sort_index: knownDatatypes [ + (knownDatatypes occurrencesOf: self) = 1 ifFalse: [ self error: 'One and only one occurrence of each datatype is expected' ]. + ^{nil . (knownDatatypes indexOf: self) - 1} +] diff --git a/src/Z3/Z3Sort.class.st b/src/Z3/Z3Sort.class.st index bf258e9ea..14de1ab1e 100644 --- a/src/Z3/Z3Sort.class.st +++ b/src/Z3/Z3Sort.class.st @@ -169,3 +169,8 @@ Z3Sort >> numeralFrom: aString [ Z3Sort >> raisedTo: B [ ^B ==> self ] + +{ #category : #'recursive adt' } +Z3Sort >> sort_index: _ [ + ^{self . 0} +]