fix(Inference): Work harder in variable instantiation

[croyzor]

Extend the instantiate_variables method in extension inference to handle the case where we end up with variables which form loops of Plus constraints with other metavariables. This is required to get the rest of the test variants in test_cfg_loops to work

Resolves #598

[acl-cqc]

So it's not clear to me from this what happens when we call self.get_constraints(m) for an m that we've seen before (on a previous iteration of the outermost loop). Will we get anything back? If so, is there any chance that we'll actually get a new thing to add to variable_scope? Or is it only the new/never-seen-before values of m that lead to finding new things? The latter would allow us to rewrite this loop much more simply but I don't know whether it's true....

[croyzor]

I think it's the latter - if we process an m we've seen before, we'll see all the same constraints and redundantly add them to the variable_scope set

[acl-cqc]

Ok, so if each iteration made a set of new stuff to process in the next iteration, you could do away with the sizes and just have two sets - something like

let mut seen_variable_scope = HashSet::new();
let mut new_variables = self.variables.clone();
while !new_variables.empty() {
   let mut newer_variables = HashSet::new();
   for m in new_variables.iter() {
      ....add to newer_variables....
   }
   seen_variable_scope.extend(new_variables);
   new_variables = newer_variables
}

Moreover, this'll change your algorithm from O(n^2) to something closer to linear, so....

[acl-cqc]

Or have a Set (processed and finished with) and a VecDeque (queue), and add to the queue only if not previously in the set (if seen.insert(n) { queue.push(n); } sort of thing) - then you can do while let Some(m) = queue.pop() which is pretty neat

[croyzor]

I've gone for the former

[acl-cqc]

The thing that bothers me a bit here is that we don't have much of a guarantee that relations.ccs() contains every node that we didn't add a solution for earlier. (That guarantee comes from the idea that only if there was a cyclic dependency would we have failed to find a solution earlier, so every node added to relations must be in a cycle, but still.)

One possible answer?? Don't mutate via self.add_solution but return a complete Map. Then you can assert that the map has the right number of entries (same as variable_scope.len()). Then you can add that Map to self.solutions all in one go (after debug_assert!ing that the keyset is disjoint, as per fn add_solution)

[acl-cqc]

(There are other ways, you could record the ms for which the first loop failed to find a solution, then tick them off here. But that'd be more expensive when debug_assert is disabled)

[croyzor]

We could add an assert that the number of nodes in relations.css() (flattened) is the same as the length of variable_scope?

[acl-cqc]

You'd need to filter out the number of those that were already in self.solved (there's an if !self.solved.contains)...

But the flattening idea is good - how about just that the number of nodes in flattened-relations.css() is equal to the number of edges in relations?

[acl-cqc]

Ah ok, some edges share endpoints. This works:

Suggested change

	for cc in relations.ccs() {
	assert_eq!(relations.node_map.len(), relations.ccs().iter().map(Vec::len).sum::<usize>());

Common up the two relations.ccs tho!

[croyzor]

I'm not sure that check really makes sense, since it's apparent that the size of node_map and the number of nodes in the graph will be the same from looking at GraphContainer::add_or_retrieve, and sccs will return a clustered version of every node in the graph

[acl-cqc]

Agreed size of node map equals number of nodes in the graph, yes the latter is what I meant.

But SCC = Strongly Connected Component, i.e. every node reaches every other? In a directed graph? Ah, are ccs undirectly-connected?

So A -> B -> C -> A is one SCC, with all three nodes. But A -> B -> C is NOT an SCC by that definition, but are you saying that .ccs() would give you [[A],[B],[C]]?

[acl-cqc]

Yes, indeed it does. In which case yeah, no assert/check really seems necessary, we're only really protecting against somehow getting in a muddle ourselves between the two loops.

Does make me wonder whether we could just put everything through the relations map, then. A node with no connections will trivially (and cheaply) be its own SCC. So this above:

if unresolved_metas,is_empty() {
   self.add_solution(m, solution.clone())
} else {
  unresolved_metas.iter().for_each(.....)
}

could just be

relations.add_or_retrieve(m);
unresolved_metas.iter().for_each(....)

and then all the add_solution calls would be in the second loop.

[acl-cqc]

Hahaha! Neat :-) You might consider flat_map (*3) to avoid mut but like it either way :)

[acl-cqc]

Thanks Craig - looks good to me, some minor suggestions

[acl-cqc]

We don't need to add to solutions here do we? What if we had, say, two SCCs with an edge between them:

A -> B -> C -> A
D -> E -> F -> D
A -> D

I note Petgraph's tarjan_scc returns the components in a defined order (reverse topsort or something), so in theory (maybe you have to reverse cc) it's soluble, but I think you need to consider not just solutions.get(m) for each m in the SCC but the solutions to the constraints upon m (which by that topsort ordering have already been computed).

Or, maybe such a structure can't occur, I dunno....????

[acl-cqc]

Try branch inference-variable/fix-dependent-sccs (the last commit) - some uncertainties detailed in the comments there, and needs a test of a structure such as the ABCDEF above.

[acl-cqc]

Ooops, realize that wasn't passing tests! A missed self.resolve should make it pass now.

[acl-cqc]

Also, I have been wondering. Why is it sufficient to do this in instantiate_variables?

Firstly, shouldn't we include Metas 'solved' by finding they are in cycles, in the solution rather than the closure? But secondly, is it actually sufficient. Or, should we detect cycles of plus constraints earlier - perhaps before the first main_loop - and then convert them to equality constraints?