Proof Slicer always active

[unp1]

Description

The dependency tracking of the proof slicer is always active even during automatic proof search.

Additional information

The implementation of ruleApplied() contains several loops, hence, this could be a performance issue.
The other reason (and why I looked at it), if something goes wrong there, the proof cannot be continued.

My suggestions would be:

• listen to the event for autoModeStarted() and unregister when that happens (when it restart the analysis needs to be rebuild or one can store at the starting event the relevant nodes and then replay from there?)
• allow the user to diconnect from the dependency tracking (unchecking the dependency tracking checkbox, does not unregister the listener)
• Question: Would it be possible to do the dependency tracking first once we decide to slice proof?

---

• Commit:

[FliegendeWurst]

Question: Would it be possible to do the dependency tracking first once we decide to slice proof?

I think there was a reason I didn't implement it this way in the first place. But I will check again.

[FliegendeWurst]

Question: Would it be possible to do the dependency tracking first once we decide to slice proof?

I think there was a reason I didn't implement it this way in the first place. But I will check again.

Just had a look. It seems it is just easier to gather the data using RuleAppInfo (added/removed formulas). It's definitely possible to construct the dependency graph without running the tracker all the time.

The implementation of ruleApplied() contains several loops, hence, this could be a performance issue.

I did some profiling recently and the dependency tracking had almost no impact on performance (<1%). The runtime is approximately O(input formulas * output formulas) per node.
But it is indeed possible that the tracking code could throw an exception.

There is one benefit of always tracking dependencies: the "show proof step that created this formula" action isn't available otherwise.