Rewriting/expanding definitions (performance)

[Giulia Sindoni]

Hi everyone,

I’m developing a pvs strategy and I have noticed that the bottleneck of it is when I need to rewrite/expand definitions.

I have experimented with different ways rewriting definitions, and I found that the rule (auto-rewrite-theory <theory name>) followed by (do-rewrite) is more efficient than using (expand <functionname>), in my case. But still, this is the bottleneck of my strategy. 

I do work with quite large formulae. But I find it odd that rewriting a formula of a certain size (where by size I mean the number of connectives that need rewriting) is much slower than performing other steps seemingly more complex (for example doing actual deduction using some deduction procedure on the same big formula is reasonably quick,  once the formula has been rewritten/expanded but the size in terms of boolean connectives is the same,). 

Does anyone have similar experience when working with large formulae? Is it something that can be addressed so to improve the overall performance of the strategy?

Thanks a lot for this very useful group and community!

Giulia