If we already know it's #===, create PAtom early

shingarov · Oct 24, 2024 · 9e75b9e · 9e75b9e
1 parent f09f5ed
commit 9e75b9e
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 1 deletion.
diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st
@@ -118,7 +118,7 @@ Expr >> <=> rhs [
 { #category : #'theory symbols' }
 Expr >> === rhs [
 	^ECst
-		expr: (EMessageSend of: (MessageSend receiver: self selector: #=== argument: rhs))
+		expr: (PAtom brel: #=== x: self y: rhs)
 		sort: Bool sort
 ]
 

diff --git a/src/Refinements/PAtom.class.st b/src/Refinements/PAtom.class.st
@@ -69,6 +69,19 @@ PAtom >> brel: anObject [
 	brel := anObject
 ]
 
+{ #category : #elaboration }
+PAtom >> elab: f [
+	| x′ y′ computed |
+	brel = Ueq ifTrue: [ self shouldBeImplemented ]. "| r == Ueq || r == Une = do…"
+	brel = Ueq ifTrue: [ self shouldBeImplemented ].
+
+	"elab f@(env,_) (PAtom r e1 e2)"
+	x′ := (x elab: f) first.
+	y′ := (y elab: f) first.
+	computed := x′ perform: brel with: y′.
+	^{ computed . Bool sort }
+]
+
 { #category : #'term rewriting' }
 PAtom >> evaluateIn: aBindEnv ifUndeclared: vndBlock [
 	^(x evaluateIn: aBindEnv ifUndeclared: vndBlock)
@@ -97,6 +110,11 @@ PAtom >> printOn: aStream [
 	aStream nextPut: $).
 ]
 
+{ #category : #'SMT interface' }
+PAtom >> smt2 [
+	^x smt2 perform: brel with: y smt2
+]
+
 { #category : #'term rewriting' }
 PAtom >> subst1: θ [ 
 	^PAtom