-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Repeats in sentence letter evaluation #28
Comments
That's great! This is a good report. I agree that it's low priority. I'll add it to the optimization TODOs to come back to at some point. |
Just putting this here for further documentation of why this is not an issue: Put in these inputs:
Wrote this up in
The comments go through this reasoning too, but here it is in prose. A new instance of an AtomSort is made (line 1 of the |
I'm thinking that if Z3 has the ability to "collapse" multiple instances of a Sort into one if they have the same "name", then it's a feature that Z3 people expect to be useful and used, and thus have probably optimized it. I am partially just trying to justify not changing the way it is now because changing it would mean we'd need to change where prefix sentences are defined and move functions around that right now are in nice places, but I do think it can (and maybe should, because it's more understandable) be kept like this for now |
That all sounds good to me. This might make for a good issue to raise with a Z3 expert at some point. |
Hey Ben, I did some more poking around and I think that the multiple sentence letter occurrence issue I mentioned is not a problem. Look at this code:
Seems that even though
A
is not the same. object asB
in the computer's memory (whatis
tests for), Z3—as you suggested—somehow knows that these two refer to the same Z3 sentence (one that's a TestSort and is represented by'A'
). I think this is now a lower priority issue.The text was updated successfully, but these errors were encountered: