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§ Source

If 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.