Sharing of subterms
#773
-
|
Hello. Z3 just expands the |
Beta Was this translation helpful? Give feedback.
Answered by
blishko
Sep 20, 2024
Replies: 1 comment
-
|
Internally, each term in OpenSMT is unique. When it is shared as a subterm in multiple terms, each term only has a "reference" ( |
Beta Was this translation helpful? Give feedback.
0 replies
Answer selected by
bruderj15
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Internally, each term in OpenSMT is unique. When it is shared as a subterm in multiple terms, each term only has a "reference" (
PTRef) to the unique term.I would say this is similar to Z3 (although the implementation details are different, I would say).
letsare only handled by the SMT-LIB frontend, they do not exist internally.