Repeats in sentence letter evaluation

[mbuit82]

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:

TestSort = DeclareSort('Test')
A = Const('A', TestSort)
B = Const('A', TestSort)
C = Const('C', TestSort)
print(A is B) # comes out False—this means that A and B are assigned to different objects in the computer's memory
print(A == B) # comes out as a Z3 constraint, which makes sense because == has a special meaning for Z3
print(simplify(A == B)) # comes out True—means that Z3 somehow knows that these two are the same
print(simplify(A == C)) # comes out as a Z3 constraint, which I think makes sense;
# since A is not necessarily equivalent to C, Z3 only simplifies it to a constraint, but in the previous
# case, it did manage to simplify it completely because it realizes that the 'name' part of the two
# sentences are the same (so presumably it collapses them?)

Seems that even though A is not the same. object as B in the computer's memory (what is 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.

[benbrastmckie]

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.

[mbuit82]

Just putting this here for further documentation of why this is not an issue:

Put in these inputs:

premises = ['ball_is_red', '(ball_is_red rightarrow neg mary_likes_it)']
conclusions = ['mary_likes_it']

Wrote this up in test.py (which is meant to simulate what using the package in a python file would be like) (also note this is just the relevant part of the file—premises, conclusions, and bools are defined above this chunk):

mod = make_model_for(N)(premises, conclusions)
mod.solve()
mod.print_to(print_cons_bool, print_unsat_core_bool, True)
if mod.model_status:
    A = Const('ball_is_red', AtomSort)
    print(mod.find_proposition_object(str(A), prefix_search=False))
    red_prop = mod.find_proposition_object([A], prefix_search=True) # it finds a Proposition object
    print([bitvec_to_substates(ver, mod.N) for ver in red_prop['verifiers']])
    # prints ['b.c', 'a.b.c', 'b', 'a', 'c', 'a.c', 'a.b']
    # so moreover, that Proposition object (red_prop) has the same verifiers as the one printed by
    # the model before

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 if statement). If a Proposition object can be found that matches the AtomSort using prefix_search (third line of the if statement), then (in very non-technical terms) it seems Z3 collapses this new AtomSort with an old call of the AtomSort (further evidence this whole thing is not a problem). However if a Proposition object cannot be found, then we have a problem. A proposition object was found, so it further seems like we don't have a problem.

[mbuit82]

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

[benbrastmckie]

That all sounds good to me. This might make for a good issue to raise with a Z3 expert at some point.