Mangle uses seminaive evaluation which is a standard, not very fancy but incremental way of computing fixpoint. I believe Datafun uses the same but there it req

Mangle uses seminaive evaluation which is a standard, not very fancy but incremental way of computing fixpoint. I believe Datafun uses the same but there it requires more thinking since it interacts with other language features. I need to reread the paper. There are really many low level ways to optimize incremental fixpoint computation in practice since the key step involves a look up whether a fact has already been computed. However, having evaluation access the FactStore through an interface means a developer can hook up various implementations and that flexibility can matter more than the last bit of performance.