The fixed point computation is performing redundant computations. insertTuplestoHead function is taking almost 70% of the time even though it shouldn't be the bottleneck. There are some issues in our current implementation:
Currently we merge tuples of head table during each execution. However, we only need to merge tuples when we are checking if the initialized head is contained within the generated head
When adding generated answer to the head in insertTuplesToHead, we only need to add distinct tuples. (A future optimization might be to not even add repeated tuples in faure evaluation)
Checking for tuple equivalence in Z3 can be simply a string comparison. A possible optimization with BDD would be to keep track of string conditions along with the integer ids.
We check if the head is contained at the end of the fixed point now since we want to avoid doing merge tuples operations as much as we can
The fixed point computation is performing redundant computations. insertTuplestoHead function is taking almost 70% of the time even though it shouldn't be the bottleneck. There are some issues in our current implementation:
(Issue created to keep track of enhancements)