Open
Description
I was wondering if I have a large term phi that contains an FNode like:
lhs = Read(Write(client-1, x-1, False) Y-1)
and I want to rewrite the whole term to:
rhs = Read(client-1, Y-1)
Why can't I run:
phi.substitute({lhs: rhs})
It seems that I should be able to do that, but I think PySmt wants me to provide an interpretation for Read generally, but I don't want to do that because I don't want to rewrite all Read terms, just this one specifically.
Metadata
Metadata
Assignees
Labels
No labels