Fixpoint3.ProvenanceReconstruct
This module reconstructs the proof tree given a provenance model. It does so by re-evaluating the program in a top-down fashion to prove the sought after atom. This search is augmented with knowledge about which facts are true and the rules used to construct them.
The current implementation assumes that all negative atoms are placed after positive atoms. More precicely it assumes that all variables in the negative atoms have been bound if a rule is evaluated left to right.
The current implementation assumes that guards satisfy the same property as the negative atoms, namely that all their variables are bound when they are encountered when evaluating a rule left to right.
The current implementation does not output the negative atoms. They can be derived from the positive.
Definitions
def provQuery(predSym: PredSym, fact: Vector[Boxed], withh: Vector[PredSym], d: Datalog): Option[Vector[(PredSym, Vector[Boxed])]]
SourceReturns None if predSym(fact) is not a part of the provenance model d.
Returns Some(v) where v is a vector of the facts that can be used to prove fact.
In other words they are the result of flattening the proof tree of predSym(fact).
Crashes if d is not a provenance model.