Fixpoint3.Phase.ProvenanceAugment
This module augments the program to track when and how facts were created.
EDB facts will be augmented with time/depth 0 and rule -1.
The program is augmented to compute ensure that computed facts track which rule created them and at which depth they were time/created.
Time/depth should be understood as follows: If a fact depend on some fact
which has time/depth k then this facts has at most time/depth k + 1.
This module removes BoolExp.NotMemberOf as the ProvProject introduced by Lowering
must ensure this property. Note that only this does not refers to the NotMemberOf relating
to negative dependencies/the not A(...) constructs.
Definitions
def augmentProgram(withProv: Bool, program: RamProgram): RamProgram
SourceIf withProv is False: program is returned unchanged.
If withProv is True: Augment program to maintain proof depth of atoms and
rule used to generate them. Further add extend facts to contain a depth and rule.