search

salmans / Razor

5 stars 0 forks source link

origin* command does not highlight / explain equivalence class information properly #52

Closed thedotmatrix closed 9 years ago

thedotmatrix commented 9 years ago

For example, if the equivalence class members for e^0 are e^0 and e^1. asking for the origin* e^0 should display two provenance sequents: one for e^0, one for e^1, which happens to be an alternate name for e^0.

Right now, origin* does that, but it restates "origin of e^0" instead of e^1. There should also be some verbosity to explaining clearly that only e^0 is an element in the model, e^0 and e^1 are named by e^0, and that they were collapsed during the SMT process.

thedotmatrix commented 9 years ago

This is an issue with blame as well. e^1 is really just another name for the actual element e^0. This detail should not be exposed to the user, as the model collapses these names into the element, and as far as they are concerned, only e^0 exists.

origin and blame information should "rename" any of the equivalent names of elements to the name of the element in the model.