In the SCION code, when I have a couple of modules, each of which may import some other modules, it seems that many many many identical constraints are added to the SMT problem multiple times. Is it possible that this happens
when multiple modules import the same other module?
when methods/... are inherited in one class from another? Do we run the inference separately on the copied version?
I think the inference should run exactly once on each module, no matter how many other modules import it, and once on each method, no matter how often it is inherited. I think especially the former is one of the main reasons why the inference on SCION code is currently slow.
In the SCION code, when I have a couple of modules, each of which may import some other modules, it seems that many many many identical constraints are added to the SMT problem multiple times. Is it possible that this happens
I think the inference should run exactly once on each module, no matter how many other modules import it, and once on each method, no matter how often it is inherited. I think especially the former is one of the main reasons why the inference on SCION code is currently slow.