search

GaloisInc / what4

Symbolic formula representation and solver interaction library
154 stars 13 forks source link

Do bound variables need annotations? #244

Closed langston-barrett closed 11 months ago

langston-barrett commented 11 months ago

The annotation mechanism (annotateTerm) attaches Nonces to expressions via the Annotation constructor of NonceApp. Bound variables already have associated Nonces, their bvarIds. We should consider whether annotateTerm, when applied to a BoundExpr, should return the term as-is, and getAnnotation could just return the bvarId.

RyanGlScott commented 11 months ago

Yes, this seems wise. We already do something similar for NonceAppExprs here:

https://github.com/GaloisInc/what4/blob/076f49b996bd328764a9c6edece6b7c34cb1cfb4/what4/src/What4/Expr/Builder.hs#L1640-L1643

langston-barrett commented 11 months ago

We already do something similar for NonceAppExprs here:

I'm not sure this is analogous, actually - that case seems to be for Annotation expressions, which are explicitly annotated (unlike BoundVarExprs, which are kind of "implicitly" annotated by virtue of already having a Nonce). However, we could probably special-case NonceAppExpr more generally in the same way - see #246.