[optimization] differential rule applications

[bddap]

The core reasoner (currently called TripleStore) is only capable of doing a round of reasoning over all tuples at once. This is optimal for the first round of reasoning, but causes a lot of re-computation during subsequent rounds.

If proof generation speed is found to be an issue, this optimization should be implemented:

Instead of, or in addition to fn apply. Add a function called e.g. insert_apply:

pub fn insert_apply(
    &self,
    triple: Triple,
    rule: &mut [Triple],
    instantiations: &mut Instantiations,
    cb: &mut impl FnMut(&Instantiations),
);

insert_apply can skip much of the wasted computation by assuming that the tuples stored in self have already been processed that the provided triple is the only potentially novel fact.

Alternate, and possibly more efficient, versions of insert_apply:

pub fn insert_apply(
    &self,
    triples: &[Triple],
    rule: &mut [Triple],
    instantiations: &mut Instantiations,
    cb: &mut impl FnMut(&Instantiations),
);

pub fn insert_apply(
    &self,
    other: &TripleStore,
    rule: &mut [Triple],
    instantiations: &mut Instantiations,
    cb: &mut impl FnMut(&Instantiations),
);

For that last one, insert_apply may assume that other is already processed or may process other itself. That last one is effectively a binary operation that merges two triple stores together, making deductions in the process. It could be used to recursively build a larger TripleStore out of smaller ones.