From 6119cddbd2e030d58a821a89dd89b8a8d7bd8800 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Wed, 9 Oct 2024 06:08:11 -0400 Subject: [PATCH 01/10] Pass the SymEnv into #sort: indirectly through Reader Thus, the keyword #smt2: is gone in favor of unary #smt2. This has the advantage that we don't have to lug the SymEnv as argument to unFApp, z3sort etc. --- src/PLE/Equation.extension.st | 2 +- src/Refinements/BindEnv.class.st | 4 ++-- src/Refinements/ECst.class.st | 10 +++++----- src/Refinements/EIte.class.st | 8 ++++---- src/Refinements/EMessageSend.class.st | 6 +++--- src/Refinements/EVar.class.st | 7 +++++-- src/Refinements/Expr.class.st | 6 +++--- src/Refinements/Integer.extension.st | 2 +- src/Refinements/PAnd.class.st | 4 ++-- src/Refinements/PKVar.class.st | 2 +- src/Refinements/PNot.class.st | 6 ++++++ src/Refinements/POr.class.st | 4 ++-- src/Refinements/Reft.class.st | 4 ++-- src/Refinements/SInfo.class.st | 17 +++++++++++------ src/Refinements/SimpC.class.st | 4 ++-- src/Refinements/Solution.class.st | 11 +++++++---- src/Refinements/SortedReft.class.st | 4 ++-- src/Refinements/UncurriedApp.class.st | 12 ++++++------ src/Refinements/Z3AST.extension.st | 2 +- src/Refinements/Z3Node.extension.st | 2 +- 20 files changed, 67 insertions(+), 50 deletions(-) diff --git a/src/PLE/Equation.extension.st b/src/PLE/Equation.extension.st index 9bbb9fd1d..dae6ec364 100644 --- a/src/PLE/Equation.extension.st +++ b/src/PLE/Equation.extension.st @@ -19,7 +19,7 @@ instance Normalizable Equation where x suffixSymbol: (eqName intSymbol: i) ]. evalEnv := EvalEnv ofSorts: (SEnv newFromAssociations: eqArgs), sEnv naturalTransformations. body′ := eqBody evaluateIn: evalEnv. - body′ := body′ smt2: sEnv. + body′ := [ body′ smt2 ] runReader: #symbolEnv initialState: sEnv. su := Dictionary newFromAssociations: (xs zip: xs′). body′ := body′ renameVariables: su. body′ := body′ normalizeBody: eqName. diff --git a/src/Refinements/BindEnv.class.st b/src/Refinements/BindEnv.class.st index 02d146d27..ca4834e4c 100644 --- a/src/Refinements/BindEnv.class.st +++ b/src/Refinements/BindEnv.class.st @@ -199,10 +199,10 @@ In Smalltalk we destructively replace the indexDict in-place. ] { #category : #'SMT interface' } -BindEnv >> smt2: γ [ +BindEnv >> smt2 [ self mapBindEnv: [ :i :x_sr | | x sr | x := x_sr key. sr := x_sr value. - x -> (sr smt2: γ) ] + x -> sr smt2 ] ] { #category : #accessing } diff --git a/src/Refinements/ECst.class.st b/src/Refinements/ECst.class.st index 031433c6f..a4072c3df 100644 --- a/src/Refinements/ECst.class.st +++ b/src/Refinements/ECst.class.st @@ -124,17 +124,17 @@ ECst >> printUncastOn: aStream [ ] { #category : #'SMT interface' } -ECst >> smt2: γ [ +ECst >> smt2 [ | fxyz f args | (sort isKindOf: FFunc) ifTrue: [ | nt uncurriedSort | (expr isKindOf: EVar) ifFalse: [ self error "monkey programmer at work" ]. - nt := γ naturalTransformationFor: expr sym. + nt := (Context readState: #symbolEnv) naturalTransformationFor: expr sym. uncurriedSort := sort uncurry. ^nt from: uncurriedSort dom to: uncurriedSort cod ]. - (expr isKindOf: EApp) ifFalse: [ ^expr smt2Cast: sort in: γ ]. + (expr isKindOf: EApp) ifFalse: [ ^expr smt2Cast: sort ]. "TODO: Investigate why control can reach here. See Issue#272." @@ -142,8 +142,8 @@ ECst >> smt2: γ [ "(ECst (EApp...)): Possibly need to uncurry." fxyz := self splitArgs. - f := fxyz key smt2: γ. - args := fxyz value collect: [ :eachArg | eachArg key smt2: γ ]. + f := fxyz key smt2. + args := fxyz value collect: [ :eachArg | eachArg key smt2 ]. ^f valueWithArguments: args ] diff --git a/src/Refinements/EIte.class.st b/src/Refinements/EIte.class.st index 8ec4d4853..f8d7e5438 100644 --- a/src/Refinements/EIte.class.st +++ b/src/Refinements/EIte.class.st @@ -80,10 +80,10 @@ EIte >> evaluateIn: anEvalEnv ifUndeclared: vndBlock [ ] { #category : #'SMT interface' } -EIte >> smt2: γ [ - ^((b smt2: γ) - ifThen: (thenE smt2: γ) - else: (elseE smt2: γ) +EIte >> smt2 [ + ^(b smt2 + ifThen: thenE smt2 + else: elseE smt2 ) simplify ] diff --git a/src/Refinements/EMessageSend.class.st b/src/Refinements/EMessageSend.class.st index a54964767..464cdeca4 100644 --- a/src/Refinements/EMessageSend.class.st +++ b/src/Refinements/EMessageSend.class.st @@ -50,8 +50,8 @@ EMessageSend >> messageSend: anObject [ ] { #category : #'SMT interface' } -EMessageSend >> smt2: γ [ - ^(messageSend receiver smt2: γ) +EMessageSend >> smt2 [ + ^messageSend receiver smt2 perform: messageSend selector - withArguments: (messageSend arguments collect: [ :arg | arg smt2: γ ]) + withArguments: (messageSend arguments collect: #smt2) ] diff --git a/src/Refinements/EVar.class.st b/src/Refinements/EVar.class.st index c21f17fb5..0e9e65597 100644 --- a/src/Refinements/EVar.class.st +++ b/src/Refinements/EVar.class.st @@ -130,8 +130,11 @@ EVar >> readStream [ ] { #category : #'SMT interface' } -EVar >> smt2: aSymEnv [ - ^(aSymEnv sort at: sym) z3sort mkConst: sym +EVar >> smt2 [ + | preSort z3sort | + preSort := (Context readState: #symbolEnv) sort at: sym. + z3sort := preSort z3sort. + ^z3sort mkConst: sym ] { #category : #'SMT interface' } diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st index 60fb29298..584cb70da 100644 --- a/src/Refinements/Expr.class.st +++ b/src/Refinements/Expr.class.st @@ -428,16 +428,16 @@ Expr >> rename: a to: b [ ] { #category : #'SMT interface' } -Expr >> smt2: γ [ +Expr >> smt2 [ self shouldNotImplement ] { #category : #'SMT interface' } -Expr >> smt2Cast: _ in: γ [ +Expr >> smt2Cast: _ [ " smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder " - ^self smt2: γ + ^self smt2 ] { #category : #'as yet unclassified' } diff --git a/src/Refinements/Integer.extension.st b/src/Refinements/Integer.extension.st index 389524596..0485df0e0 100644 --- a/src/Refinements/Integer.extension.st +++ b/src/Refinements/Integer.extension.st @@ -11,7 +11,7 @@ Integer >> evaluateIn: anEvalEnv ifUndeclared: vndBlock [ ] { #category : #'*Refinements' } -Integer >> smt2: _ [ +Integer >> smt2 [ ^self toInt ] diff --git a/src/Refinements/PAnd.class.st b/src/Refinements/PAnd.class.st index c1ba10749..157114659 100644 --- a/src/Refinements/PAnd.class.st +++ b/src/Refinements/PAnd.class.st @@ -110,9 +110,9 @@ PAnd >> rename: a to: b [ ] { #category : #'SMT interface' } -PAnd >> smt2: γ [ +PAnd >> smt2 [ | cs | - cs := conjuncts collect: [ :each | each smt2: γ ]. + cs := conjuncts collect: #smt2. ^(cs allSatisfy: #isConc) ifTrue: [ Bool and: cs ] ifFalse: [ ^self class of: cs ] diff --git a/src/Refinements/PKVar.class.st b/src/Refinements/PKVar.class.st index 0ed351fbf..4f3cc265e 100644 --- a/src/Refinements/PKVar.class.st +++ b/src/Refinements/PKVar.class.st @@ -115,7 +115,7 @@ PKVar >> s: anObject [ ] { #category : #'SMT interface' } -PKVar >> smt2: _ [ +PKVar >> smt2 [ ^self ] diff --git a/src/Refinements/PNot.class.st b/src/Refinements/PNot.class.st index fc766a8e6..3589ad9aa 100644 --- a/src/Refinements/PNot.class.st +++ b/src/Refinements/PNot.class.st @@ -43,6 +43,12 @@ PNot >> printOn: aStream [ p printOn: aStream ] +{ #category : #'SMT interface' } +PNot >> smt2 [ + p isConc ifFalse: [ self shouldBeImplemented ]. + ^p smt2 not +] + { #category : #'F.Subable' } PNot >> subst1: ass [ ^PNot of: (p subst1: ass) diff --git a/src/Refinements/POr.class.st b/src/Refinements/POr.class.st index ee96808dd..9a296ebd0 100644 --- a/src/Refinements/POr.class.st +++ b/src/Refinements/POr.class.st @@ -45,9 +45,9 @@ POr >> evaluateIn: aBindEnv ifUndeclared: vndBlock [ ] { #category : #'SMT interface' } -POr >> smt2: γ [ +POr >> smt2 [ (disjuncts allSatisfy: #isConc) ifFalse: [ self shouldBeImplemented ]. - ^Bool or: (disjuncts collect: [ :each | each smt2: γ ]) + ^Bool or: (disjuncts collect: #smt2) ] { #category : #'F.Subable' } diff --git a/src/Refinements/Reft.class.st b/src/Refinements/Reft.class.st index 1add314eb..41fe9f4cf 100644 --- a/src/Refinements/Reft.class.st +++ b/src/Refinements/Reft.class.st @@ -175,10 +175,10 @@ Cf. Constraints.hs ] { #category : #'SMT interface' } -Reft >> smt2: γ [ +Reft >> smt2 [ ^Reft symbol: symbol - expr: (expr smt2: γ) + expr: expr smt2 ] { #category : #'F.Subable' } diff --git a/src/Refinements/SInfo.class.st b/src/Refinements/SInfo.class.st index ad8d069ca..5c168399e 100644 --- a/src/Refinements/SInfo.class.st +++ b/src/Refinements/SInfo.class.st @@ -193,6 +193,15 @@ SInfo >> eliminatingSolverInfo [ ] +{ #category : #'SMT interface' } +SInfo >> emitSMT2 [ + | γ | + γ := self symbolEnv. + [ γ naturalTransformations: gLits. + γ naturalTransformations freezeNaturalTransformations. + self smt2 ] runReader: #symbolEnv initialState: γ +] + { #category : #'as yet unclassified' } SInfo >> getSubC: i [ " @@ -400,12 +409,8 @@ SInfo >> sanitize [ { #category : #'SMT interface' } SInfo >> smt2 [ - | γ | - γ := self symbolEnv . - γ naturalTransformations: gLits. - γ naturalTransformations freezeNaturalTransformations. - cm do: [ :eachC | eachC smt2: γ ]. - bs smt2: γ. + cm do: #smt2. + bs smt2. ] { #category : #logic } diff --git a/src/Refinements/SimpC.class.st b/src/Refinements/SimpC.class.st index f1347169c..3daf9f36b 100644 --- a/src/Refinements/SimpC.class.st +++ b/src/Refinements/SimpC.class.st @@ -100,9 +100,9 @@ SimpC >> sinfo [ ] { #category : #'SMT interface' } -SimpC >> smt2: aSymEnv [ +SimpC >> smt2 [ "Destructively replace RHS with its Z3 AST." - rhs := rhs smt2: aSymEnv. + rhs := rhs smt2. ^self ] diff --git a/src/Refinements/Solution.class.st b/src/Refinements/Solution.class.st index fea9c3ca5..cc7c9dd3a 100644 --- a/src/Refinements/Solution.class.st +++ b/src/Refinements/Solution.class.st @@ -217,9 +217,12 @@ Solution >> qbPreds: aSubst qBind: aQBind [ qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)] Cf. Types/Solutions.hs " - | elabPred | - elabPred := [ :eq | ((eq pred subst: aSubst) elaborate: sEnv) smt2: sEnv ]. - ^aQBind eQuals collect: [ :eq | { elabPred value: eq . eq } ] + ^aQBind eQuals collect: [ :eq | + | pred smt2 | + pred := (eq pred subst: aSubst) elaborate: sEnv. + smt2 := [ pred smt2 ] runReader: #symbolEnv initialState: sEnv. + { smt2 . eq } + ] ] { #category : #'as yet unclassified' } @@ -357,7 +360,7 @@ Solution >> sScp: anObject [ Solution >> solve_: fi ks: ks wkl: w [ "cf. Solver/Solve.hs." | s1 s2 s3 s4 res₀ s3_res0 bindingsInSmt | - fi smt2. + fi emitSMT2. s1 := fi initialSolution: ks. "cf. Solve.hs" s2 := self, s1. bindingsInSmt := __binds concretePreds. diff --git a/src/Refinements/SortedReft.class.st b/src/Refinements/SortedReft.class.st index b3096ad25..c57f3a7cd 100644 --- a/src/Refinements/SortedReft.class.st +++ b/src/Refinements/SortedReft.class.st @@ -154,10 +154,10 @@ SortedReft >> shiftSR: i [ ] { #category : #'SMT interface' } -SortedReft >> smt2: γ [ +SortedReft >> smt2 [ ^SortedReft sort: sr_sort z3sort - reft: (sr_reft smt2: γ) + reft: sr_reft smt2 ] { #category : #accessing } diff --git a/src/Refinements/UncurriedApp.class.st b/src/Refinements/UncurriedApp.class.st index 6770fe22c..de132aa43 100644 --- a/src/Refinements/UncurriedApp.class.st +++ b/src/Refinements/UncurriedApp.class.st @@ -69,19 +69,19 @@ UncurriedApp >> resultSort: anObject [ ] { #category : #'SMT interface' } -UncurriedApp >> smt2: γ [ +UncurriedApp >> smt2 [ | s α D αc | s := f expr sym. - α := γ naturalTransformations at: s. - D := args collect: [ :eachArg | eachArg sort ]. + α := (Context readState: #symbolEnv) naturalTransformations at: s. + D := args collect: #sort. αc := α from: D to: resultSort. - ^αc valueWithArguments: (args collect: [ :eachArg | eachArg smt2: γ ]) + ^αc valueWithArguments: (args collect: #smt2 ) ] { #category : #'SMT interface' } -UncurriedApp >> smt2Cast: s in: γ [ +UncurriedApp >> smt2Cast: s [ self assert: self resultSort = s. - ^self smt2: γ + ^self smt2 ] diff --git a/src/Refinements/Z3AST.extension.st b/src/Refinements/Z3AST.extension.st index 13f36cf4f..3ddaee18e 100644 --- a/src/Refinements/Z3AST.extension.st +++ b/src/Refinements/Z3AST.extension.st @@ -17,6 +17,6 @@ Z3AST >> evaluateIn: aBindEnv ifUndeclared: vndBlock [ ] { #category : #'*Refinements' } -Z3AST >> smt2: _ [ +Z3AST >> smt2 [ ^self ] diff --git a/src/Refinements/Z3Node.extension.st b/src/Refinements/Z3Node.extension.st index 84b07506d..b94621eb6 100644 --- a/src/Refinements/Z3Node.extension.st +++ b/src/Refinements/Z3Node.extension.st @@ -21,7 +21,7 @@ Z3Node >> kvarsExpr [ ] { #category : #'*Refinements' } -Z3Node >> smt2Cast: aZ3Sort in: _ [ +Z3Node >> smt2Cast: aZ3Sort [ aZ3Sort = self sort ifFalse: [ self error ]. ^self ] From da0f9d821b52bb99edfbed390148dcc7001507f7 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Fri, 9 Aug 2024 14:07:17 -0400 Subject: [PATCH 02/10] Introduce classes DataCtor, DataDecl, DataField --- src/Refinements/DataCtor.class.st | 56 ++++++++++++++++++++ src/Refinements/DataDecl.class.st | 85 ++++++++++++++++++++++++++++++ src/Refinements/DataField.class.st | 45 ++++++++++++++++ 3 files changed, 186 insertions(+) create mode 100644 src/Refinements/DataCtor.class.st create mode 100644 src/Refinements/DataDecl.class.st create mode 100644 src/Refinements/DataField.class.st diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st new file mode 100644 index 000000000..098d95f92 --- /dev/null +++ b/src/Refinements/DataCtor.class.st @@ -0,0 +1,56 @@ +" +data DataCtor = DCtor + { dcName :: !LocSymbol -- ^ Ctor Name + , dcFields :: ![DataField] -- ^ Ctor Fields + } deriving (Eq, Ord, Show, Data, Typeable, Generic) +" +Class { + #name : #DataCtor, + #superclass : #Object, + #instVars : [ + 'dcName', + 'dcFields' + ], + #category : #Refinements +} + +{ #category : #'instance creation' } +DataCtor class >> dcName: dcName dcFields: dcFields [ + ^self basicNew + dcName: dcName; + dcFields: dcFields; + yourself +] + +{ #category : #accessing } +DataCtor >> dcFields [ + ^ dcFields +] + +{ #category : #accessing } +DataCtor >> dcFields: anObject [ + dcFields := anObject +] + +{ #category : #accessing } +DataCtor >> dcName [ + ^ dcName +] + +{ #category : #accessing } +DataCtor >> dcName: anObject [ + dcName := anObject +] + +{ #category : #printing } +DataCtor >> printOn: aStream [ + aStream + nextPutAll: '↪'; + nextPutAll: dcName; + nextPutAll: '('. + dcFields do: + [ :df | aStream nextPutAll: df dfName; nextPutAll: '::'. df dfSort printOn: aStream ] + separatedBy: [ aStream nextPutAll: ',' ]. + aStream + nextPutAll: ')' +] diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st new file mode 100644 index 000000000..fc0bd540f --- /dev/null +++ b/src/Refinements/DataDecl.class.st @@ -0,0 +1,85 @@ +" +data DataDecl = DDecl + { ddTyCon :: !FTycon -- ^ Name of defined datatype + , ddVars :: !Int -- ^ Number of type variables + , ddCtors :: [DataCtor] -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars + } deriving (Eq, Ord, Show, Data, Typeable, Generic) +" +Class { + #name : #DataDecl, + #superclass : #Object, + #instVars : [ + 'ddTyCon', + 'ddVars', + 'ddCtors' + ], + #category : #Refinements +} + +{ #category : #'instance creation' } +DataDecl class >> ddTyCon: ddTyCon ddVars: ddVars ddCtors: ddCtors [ + ^self basicNew + ddTyCon: ddTyCon; + ddVars: ddVars; + ddCtors: ddCtors; + yourself + +] + +{ #category : #'as yet unclassified' } +DataDecl >> addToQuery: aNNFQuery [ + aNNFQuery qData add: self +] + +{ #category : #accessing } +DataDecl >> ddCtors [ + ^ ddCtors +] + +{ #category : #accessing } +DataDecl >> ddCtors: anObject [ + ddCtors := anObject +] + +{ #category : #accessing } +DataDecl >> ddTyCon [ + ^ ddTyCon +] + +{ #category : #accessing } +DataDecl >> ddTyCon: anObject [ + ddTyCon := anObject +] + +{ #category : #accessing } +DataDecl >> ddVars [ + ^ ddVars +] + +{ #category : #accessing } +DataDecl >> ddVars: anObject [ + ddVars := anObject +] + +{ #category : #GT } +DataDecl >> gtInspectorConstructorsIn: composite [ + + ^ composite fastList + title: 'Constructors'; + display: [ ddCtors ] +] + +{ #category : #printing } +DataDecl >> printOn: aStream [ + aStream nextPutAll: 'data '. + aStream nextPutAll: self ddTyCon symbol +] + +{ #category : #Symbolic } +DataDecl >> symbol [ +" +instance Symbolic DataDecl where + symbol = symbol . ddTyCon +" + ^ddTyCon symbol +] diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st new file mode 100644 index 000000000..f7aff16cc --- /dev/null +++ b/src/Refinements/DataField.class.st @@ -0,0 +1,45 @@ +" +data DataField = DField + { dfName :: !LocSymbol -- ^ Field Name + , dfSort :: !Sort -- ^ Field Sort + } deriving (Eq, Ord, Show, Data, Typeable, Generic) + + +" +Class { + #name : #DataField, + #superclass : #Object, + #instVars : [ + 'dfName', + 'dfSort' + ], + #category : #Refinements +} + +{ #category : #'instance creation' } +DataField class >> dfName: dfName dfSort: dfSort [ + ^self basicNew + dfName: dfName; + dfSort: dfSort; + yourself +] + +{ #category : #accessing } +DataField >> dfName [ + ^ dfName +] + +{ #category : #accessing } +DataField >> dfName: anObject [ + dfName := anObject +] + +{ #category : #accessing } +DataField >> dfSort [ + ^ dfSort +] + +{ #category : #accessing } +DataField >> dfSort: anObject [ + dfSort := anObject +] From 12aeecd1c8a5adfe31a9096a5e6aa65b54f2243b Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Wed, 9 Oct 2024 01:51:56 -0400 Subject: [PATCH 03/10] [cosmetic] Consistently classify #addToQuery: as 'construction' --- src/Refinements/DataDecl.class.st | 2 +- src/Refinements/Equation.class.st | 2 +- src/Refinements/HCon.class.st | 2 +- src/Refinements/HCstr.class.st | 2 +- src/Refinements/HVar.class.st | 2 +- src/Refinements/Qualifier.class.st | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st index fc0bd540f..d4996668d 100644 --- a/src/Refinements/DataDecl.class.st +++ b/src/Refinements/DataDecl.class.st @@ -26,7 +26,7 @@ DataDecl class >> ddTyCon: ddTyCon ddVars: ddVars ddCtors: ddCtors [ ] -{ #category : #'as yet unclassified' } +{ #category : #construction } DataDecl >> addToQuery: aNNFQuery [ aNNFQuery qData add: self ] diff --git a/src/Refinements/Equation.class.st b/src/Refinements/Equation.class.st index f3364ba7b..42557b50b 100644 --- a/src/Refinements/Equation.class.st +++ b/src/Refinements/Equation.class.st @@ -38,7 +38,7 @@ mkEquation f xts e out = Equ f xts e out (f `elem` syms e) yourself ] -{ #category : #adding } +{ #category : #construction } Equation >> addToQuery: aHornQuery [ aHornQuery qEqns add: self ] diff --git a/src/Refinements/HCon.class.st b/src/Refinements/HCon.class.st index e6f794deb..0dd39765d 100644 --- a/src/Refinements/HCon.class.st +++ b/src/Refinements/HCon.class.st @@ -21,7 +21,7 @@ HCon class >> symbol: sym sort: srt [ yourself ] -{ #category : #logic } +{ #category : #construction } HCon >> addToQuery: aHornQuery [ aHornQuery qCon at: symbol put: sort ] diff --git a/src/Refinements/HCstr.class.st b/src/Refinements/HCstr.class.st index 546b578ee..ae1b13f53 100644 --- a/src/Refinements/HCstr.class.st +++ b/src/Refinements/HCstr.class.st @@ -46,7 +46,7 @@ HCstr >> & anotherCstr [ ^CstrAnd of: { self . anotherCstr } ] -{ #category : #logic } +{ #category : #construction } HCstr >> addToQuery: aNNFQuery [ aNNFQuery qCstr add: self ] diff --git a/src/Refinements/HVar.class.st b/src/Refinements/HVar.class.st index f68d26056..900e81e6b 100644 --- a/src/Refinements/HVar.class.st +++ b/src/Refinements/HVar.class.st @@ -34,7 +34,7 @@ HVar class >> name: aString argSorts: sorts [ yourself ] -{ #category : #adding } +{ #category : #construction } HVar >> addToQuery: q [ q addVar: self ] diff --git a/src/Refinements/Qualifier.class.st b/src/Refinements/Qualifier.class.st index 72111f26a..00633387e 100644 --- a/src/Refinements/Qualifier.class.st +++ b/src/Refinements/Qualifier.class.st @@ -24,7 +24,7 @@ Qualifier class >> true [ ^self name: 'QTrue' params: #() body: nil ] -{ #category : #'as yet unclassified' } +{ #category : #construction } Qualifier >> addToQuery: q [ q qualifiers add: self ] From 10eafdaa0ef67796578d752e773f68332003313e Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Fri, 9 Aug 2024 14:19:51 -0400 Subject: [PATCH 04/10] =?UTF-8?q?Implement=20parsing=20of=20(data=E2=80=A6?= =?UTF-8?q?)=20in=20NNF=20queries?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Refinements-Parsing/NNFParser.class.st | 34 ++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st index 37a34b53f..7848fe56b 100644 --- a/src/Refinements-Parsing/NNFParser.class.st +++ b/src/Refinements-Parsing/NNFParser.class.st @@ -25,7 +25,8 @@ Class { 'cstrPred', 'funcSort', 'sortArg', - 'define' + 'define', + 'data' ], #category : #'Refinements-Parsing' } @@ -79,6 +80,35 @@ NNFParser >> cstrPred [ ^pred parens ==> [ :x | CstrHead pred: x ] ] +{ #category : #grammar } +NNFParser >> data [ + ^'data' asParser trim, + self fTyCon trim, + (#digit asParser plus flatten trim ==> #asInteger), + $= asParser trim, + ($| asParser trim, self dataCtor trim ==> #second) star brackets + ==> [ :x | DataDecl + ddTyCon: x second + ddVars: x third + ddCtors: x fifth ] + +] + +{ #category : #grammar } +NNFParser >> dataCtor [ + ^NNFParser upperId trim, + (self dataField commaSeparated optional ==> [ :x | x ifNil: [#()] ifNotNil: [x] ]) braces + ==> [ :x | DataCtor dcName: x first dcFields: x second ] +] + +{ #category : #grammar } +NNFParser >> dataField [ + ^ NNFParser upperId trim, + $: asParser trim, + sort + ==> [ :x | DataField dfName: x first dfSort: x last ] +] + { #category : #grammar } NNFParser >> decidablePred [ ^matchedParen @@ -234,7 +264,7 @@ NNFParser >> symSort [ { #category : #grammar } NNFParser >> thing [ - ^(constraint / var / qualif / constant / fixpoint / define "match data") parens + ^(constraint / var / qualif / constant / fixpoint / define "/ match" / data) parens ] { #category : #'grammar - util' } From c66967064a2dc59fe91ada506b11a178066af2b9 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Fri, 9 Aug 2024 14:24:07 -0400 Subject: [PATCH 05/10] First attempt to add testL5cons00data --- .../SpriteHornPosTest.class.st | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st index bf961dc93..b9fca9f6f 100644 --- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st @@ -746,6 +746,33 @@ SpriteHornPosTest >> testL5cons00 [ ] +{ #category : #'tests-L5' } +SpriteHornPosTest >> testL5cons00data [ + self provePos: ' +(var $k3 ((`a) ((`L `a)) (`a))) +(var $k1 ((`a) (`a))) + +(constant len (func(1 , [(`L @(0)); int]))) + +(data L 1 = [ + | Nil {} + | Cons {Cons0 : @(0), Cons1 : (L @(0))} + ]) + +(constraint + (forall ((x `a) (Bool true)) + (forall ((t (`L `a)) ((len value: t) === 0)) + (and + (forall ((VV `a) (VV === x)) + (($k3 VV t x))) + (forall ((VV0 `a) ($k1 VV0 x)) + (($k3 VV0 a x))) + (forall ((v (`L `a)) ((len value: v) === (1 + (len value: t)))) + ((((len value: v) === 1)))))))) +' + +] + { #category : #'tests-L5' } SpriteHornPosTest >> testL5foldRight00 [ self provePos: ' From 8cf06f073500306e8011096d14e6e748c68f19bd Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Thu, 12 Sep 2024 01:56:02 -0400 Subject: [PATCH 06/10] Add SpriteHornPosTest>>testL8uniqueVoid --- src/SpriteLang-Tests/SpriteHornPosTest.class.st | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st index b9fca9f6f..3ff7acffa 100644 --- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st @@ -1630,3 +1630,18 @@ SpriteHornPosTest >> testL7sumAcc [ & (v < n)))))))))))))) ' ] + +{ #category : #'tests-L8' } +SpriteHornPosTest >> testL8uniqueVoid [ + "Cf. liquid-fixpoint/doodles/L8uniqueVoid.smt2 on branch experiment-z3datatypes" + self provePos: ' +(data V 0 = [ + | Nil {} + ]) + +(constraint + (forall ((a V) (Bool true)) + (forall ((b V) (Bool true)) + ((a === b))))) +' +] From 3668abe6fa2d1d3d7aef63187eda68328895e149 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Fri, 20 Sep 2024 03:48:36 -0400 Subject: [PATCH 07/10] more experiments with SpriteHornTests re: data --- .../SpriteHornPosTest.class.st | 26 ++++++++++++++++--- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st index 3ff7acffa..a22534202 100644 --- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st @@ -749,10 +749,10 @@ SpriteHornPosTest >> testL5cons00 [ { #category : #'tests-L5' } SpriteHornPosTest >> testL5cons00data [ self provePos: ' -(var $k3 ((`a) ((`L `a)) (`a))) +(var $k3 ((`a) ((L `a)) (`a))) (var $k1 ((`a) (`a))) -(constant len (func(1 , [(`L @(0)); int]))) +(constant len (func(1 , [(L @(0)); int]))) (data L 1 = [ | Nil {} @@ -761,13 +761,13 @@ SpriteHornPosTest >> testL5cons00data [ (constraint (forall ((x `a) (Bool true)) - (forall ((t (`L `a)) ((len value: t) === 0)) + (forall ((t (L `a)) ((len value: t) === 0)) (and (forall ((VV `a) (VV === x)) (($k3 VV t x))) (forall ((VV0 `a) ($k1 VV0 x)) (($k3 VV0 a x))) - (forall ((v (`L `a)) ((len value: v) === (1 + (len value: t)))) + (forall ((v (L `a)) ((len value: v) === (1 + (len value: t)))) ((((len value: v) === 1)))))))) ' @@ -1171,6 +1171,24 @@ SpriteHornPosTest >> testL5tail01 [ ] +{ #category : #'tests-L5' } +SpriteHornPosTest >> testL5tail01L8 [ + self provePos: ' +(data L 1 = [ + | Nil {} + | Cons {Cons0 : @(0), Cons1 : (L @(0))} + ]) + +(constant len (func(1 , [(L @(0)); int]))) + +(constraint + (forall ((h `a) (Bool true)) + (forall ((t (L `a)) (Bool true)) + (forall ((zs (L `a)) (and ((len value: zs) > 0) ((len value: zs) === (1 + (len value: t))))) + (forall ((VV (L `a)) (VV === t)) ((((len value: VV) === ((len value: zs) - 1))))))))) +' +] + { #category : #'tests-L5' } SpriteHornPosTest >> testL5tuple00 [ self provePos: ' From a156555a3abcb35fedaea886ecbacb7f980b6b55 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Sun, 13 Oct 2024 08:17:43 -0400 Subject: [PATCH 08/10] Add Datatype tests coming from SpriteHorn doodles --- .../SpriteHornNegTest.class.st | 53 +++++++++++++++++++ .../SpriteHornPosTest.class.st | 51 ++++++++++++++++++ 2 files changed, 104 insertions(+) diff --git a/src/SpriteLang-Tests/SpriteHornNegTest.class.st b/src/SpriteLang-Tests/SpriteHornNegTest.class.st index 9c88b2da5..c7b6b888a 100644 --- a/src/SpriteLang-Tests/SpriteHornNegTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornNegTest.class.st @@ -489,3 +489,56 @@ SpriteHornNegTest >> testL6maxlist01 [ ' ] + +{ #category : #'tests-L8' } +SpriteHornNegTest >> testL8uniqueVoid2Constructors [ + self proveNeg: ' +(data V 0 = [ + | One {} + | Two {} + ]) + +(constraint + (forall ((a V) (Bool true)) + (forall ((b V) (Bool true)) + ((a === b))))) +' +] + +{ #category : #'tests-L8' } +SpriteHornNegTest >> testL8uniqueVoidNoADT [ + self proveNeg: ' +(constraint + (forall ((a `v) (Bool true)) + (forall ((b `v) (Bool true)) + ((a === b))))) +' +] + +{ #category : #'tests-L8' } +SpriteHornNegTest >> testL8uniqueVoidParam [ + self proveNeg: ' +(data V 0 = [ + | One {Cons0 : int} + ]) + +(constraint + (forall ((a V) (Bool true)) + (forall ((b V) (Bool true)) + ((a === b))))) +' +] + +{ #category : #'tests-L8' } +SpriteHornNegTest >> testL8uniqueVoidParamPoly [ + self proveNeg: ' +(data V 1 = [ + | One {Cons0 : @(0)} + ]) + +(constraint + (forall ((a (V int)) (Bool true)) + (forall ((b (V int)) (Bool true)) + ((a === b))))) +' +] diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st index a22534202..ee3b8aa02 100644 --- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st @@ -1217,6 +1217,42 @@ SpriteHornPosTest >> testL5tuple00 [ ] +{ #category : #'tests-L5' } +SpriteHornPosTest >> testL5tuple00L8 [ + self provePos: ' +IMPLEMENT ME; the Fixpoint Doodle is already pushed. +' + +] + +{ #category : #'tests-L5' } +SpriteHornPosTest >> testL5tuple00L8poly [ + self provePos: ' +(var $k1 ((int) (int) ((C int int)) (int) (int))) + +(data C 2 = [ + | C {C0 : @(0), C1 : @(1)} + ]) + +(constraint + (and + (forall ((n int) (Bool true)) + (forall ((n1 int) (n+1 === n1)) + (forall ((v int) ((n+1 === v) & (v === n1))) ((n < v))))) + (forall ((m int) (Bool true)) + (forall ((p (C int int)) (Bool true)) + (forall ((px int) (Bool true)) + (forall ((py int) (px < py)) + (forall ((p (C int int)) (Bool true)) + (and + (forall ((VV int) (VV === px)) (($k1 VV m p px py))) + (forall ((v int) ((px < v) & (v === py))) (($k1 v m p px py))) + (forall ((ok bool) (ok <=> (px < py))) + (forall ((v bool) ((v <=> (px < py)) & (v === ok))) ((v)))))))))))) +' + +] + { #category : #'tests-L6' } SpriteHornPosTest >> testL6compose00 [ self provePos: ' @@ -1663,3 +1699,18 @@ SpriteHornPosTest >> testL8uniqueVoid [ ((a === b))))) ' ] + +{ #category : #'tests-L8' } +SpriteHornPosTest >> testL8uniqueVoidExplicitDistinction [ + self provePos: ' +(data V 0 = [ + | One {} + | Two {} + ]) + +(constraint + (forall ((a V) (a === One)) + (forall ((b V) (b === One)) + ((a === b))))) +' +] From e42ed180a5a91670231d467aef31d7fc2eae694d Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Sun, 13 Oct 2024 08:31:25 -0400 Subject: [PATCH 09/10] BEGINNING IDIOTIC DOODLES --- src/Refinements/FTC.class.st | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Refinements/FTC.class.st b/src/Refinements/FTC.class.st index d095811b5..f5c317446 100644 --- a/src/Refinements/FTC.class.st +++ b/src/Refinements/FTC.class.st @@ -42,7 +42,6 @@ FTC >> containsFVar [ { #category : #hotel } FTC >> fappSmtSort: ts originalFApp: anFApp [ - | j | self isSetCon ifTrue: [ ts size = 1 ifFalse: [ self error ]. ^ts first z3sort mkSetSort @@ -50,8 +49,14 @@ FTC >> fappSmtSort: ts originalFApp: anFApp [ self isMapCon ifTrue: [ self shouldBeImplemented ]. self isBitVec ifTrue: [ self shouldBeImplemented ]. - j := PreSort hotel addElement: anFApp. - ^Z3Sort uninterpretedSortNamed: j + self maybeData + ifNil: [ + | j | + j := PreSort hotel addElement: anFApp. + ^Z3Sort uninterpretedSortNamed: j + ] ifNotNil: [ + ^self shouldBeImplemented + ] ] { #category : #comparing } @@ -83,6 +88,15 @@ Cf. fappSmtSort in Theories.hs ^typeConstructor symbol = 'Set_Set' ] +{ #category : #'as yet unclassified' } +FTC >> maybeData [ + | γ | + γ := Context readState: #symbolEnv. + ^γ data + at: typeConstructor symbol + ifAbsent: [ nil ] +] + { #category : #printing } FTC >> printOn: aStream [ aStream nextPutAll: 'FTC ('. From 10e1370d491c8e8eab4482a698cc52ea76f77d95 Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Wed, 16 Oct 2024 03:46:44 -0400 Subject: [PATCH 10/10] Naive instantiation of DataFields; doesn't handle type induction --- src/Refinements/DataCtor.class.st | 16 ++++++++++++++ src/Refinements/DataDecl.class.st | 14 ++++++++++++ src/Refinements/DataField.class.st | 8 +++++++ src/Refinements/FTC.class.st | 6 +++-- .../SpriteHornPosTest.class.st | 22 ++++++++++++++++++- 5 files changed, 63 insertions(+), 3 deletions(-) diff --git a/src/Refinements/DataCtor.class.st b/src/Refinements/DataCtor.class.st index 098d95f92..9676f82ce 100644 --- a/src/Refinements/DataCtor.class.st +++ b/src/Refinements/DataCtor.class.st @@ -54,3 +54,19 @@ DataCtor >> printOn: aStream [ aStream nextPutAll: ')' ] + +{ #category : #'as yet unclassified' } +DataCtor >> smt2ctor: ts [ + | instantiatedFields | + instantiatedFields := dcFields collect: [ :field | field dfName -> (field smt2field: ts) ]. + ^Z3Constructor + name: self symbol + recognizer: 'is-', self symbol + fields: instantiatedFields + referencing: (Array new: dcFields size withAll: 0) "BOGUS, implement mutually-recursive ADTs!" +] + +{ #category : #Symbolic } +DataCtor >> symbol [ + ^dcName +] diff --git a/src/Refinements/DataDecl.class.st b/src/Refinements/DataDecl.class.st index d4996668d..f46c065d4 100644 --- a/src/Refinements/DataDecl.class.st +++ b/src/Refinements/DataDecl.class.st @@ -69,12 +69,26 @@ DataDecl >> gtInspectorConstructorsIn: composite [ display: [ ddCtors ] ] +{ #category : #'SMT monomorphisation' } +DataDecl >> instantiateZ3Sort: ts [ + | ctors z3datatypeSort | + ctors := self smt2datactors: ts. + z3datatypeSort := Z3DatatypeSort name: self symbol constructors: ctors. + ctors do: #delete. + ^z3datatypeSort +] + { #category : #printing } DataDecl >> printOn: aStream [ aStream nextPutAll: 'data '. aStream nextPutAll: self ddTyCon symbol ] +{ #category : #'as yet unclassified' } +DataDecl >> smt2datactors: ts [ + ^ddCtors collect: [ :ctor | ctor smt2ctor: ts ] +] + { #category : #Symbolic } DataDecl >> symbol [ " diff --git a/src/Refinements/DataField.class.st b/src/Refinements/DataField.class.st index f7aff16cc..09d379fc4 100644 --- a/src/Refinements/DataField.class.st +++ b/src/Refinements/DataField.class.st @@ -43,3 +43,11 @@ DataField >> dfSort [ DataField >> dfSort: anObject [ dfSort := anObject ] + +{ #category : #'as yet unclassified' } +DataField >> smt2field: ts [ + | θ monomorphicSort | + θ := Dictionary newFromAssociations: (ts collectWithIndex: [ :t :idx | idx-1 -> t ]). + monomorphicSort := dfSort apply: θ. + ^monomorphicSort z3sort +] diff --git a/src/Refinements/FTC.class.st b/src/Refinements/FTC.class.st index f5c317446..198061bb3 100644 --- a/src/Refinements/FTC.class.st +++ b/src/Refinements/FTC.class.st @@ -54,8 +54,10 @@ FTC >> fappSmtSort: ts originalFApp: anFApp [ | j | j := PreSort hotel addElement: anFApp. ^Z3Sort uninterpretedSortNamed: j - ] ifNotNil: [ - ^self shouldBeImplemented + ] ifNotNil: [ :dataDecl | + dataDecl ddVars = ts size ifFalse: [ self error ]. + self halt. + ^dataDecl instantiateZ3Sort: ts. ] ] diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st index ee3b8aa02..e442d32b9 100644 --- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st +++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st @@ -1220,7 +1220,27 @@ SpriteHornPosTest >> testL5tuple00 [ { #category : #'tests-L5' } SpriteHornPosTest >> testL5tuple00L8 [ self provePos: ' -IMPLEMENT ME; the Fixpoint Doodle is already pushed. +(var $k1 ((int) (int) (C) (int) (int))) + +(data C 0 = [ + | C {C0 : int, C1 : int} + ]) + +(constraint + (and + (forall ((n int) (Bool true)) + (forall ((n1 int) (n+1 === n1)) + (forall ((v int) ((n+1 === v) & (v === n1))) ((n < v))))) + (forall ((m int) (Bool true)) + (forall ((p C) (Bool true)) + (forall ((px int) (Bool true)) + (forall ((py int) (px < py)) + (forall ((p C) (Bool true)) + (and + (forall ((VV int) (VV === px)) (($k1 VV m p px py))) + (forall ((v int) ((px < v) & (v === py))) (($k1 v m p px py))) + (forall ((ok bool) (ok <=> (px < py))) + (forall ((v bool) ((v <=> (px < py)) & (v === ok))) ((v)))))))))))) ' ]