Sibling-node-based cost function and indexed operators

[cgjohannsen]

Hi there! I'm looking into using egg for minimizing the encoding size of a interval-bounded temporal logic. Formulas look something like G[0,5] (p && q) meaning p or q must occur from now until 5 time steps from now.

I have two problems that, judging from previous questions and messing with examples, egg does not provide support for:

1. These formula have cost functions dependent on sibling nodes, where one node in the expression may need to store intermediate results. Is it possible to define a cost function that depends on sibling nodes?
2. The language has indexed identifiers, for example, G[0,5] vs G[2,7]. Some rewrite rules alter these indices, like the rewrite rule (G[0,5] p) && (G[0,10] p) => G[0,10] p. Is this possible to define in egg?

Are my suspicions correct? Any help would be appreciated, thanks!

[mwillsey]

Not sure what is meant by sibling node here. For part 2, I don't see a specific problem in altering the indices, as long as they are represented in the normal egraph-y way. So I assume G is a constructor with 3 arguments: two bounds and the argument. I think I'll need some more example to see what's going on.

[cgjohannsen]

Sure thing. The context here is monitoring of formulas, so we're basically incrementally evaluating these formulas over ever-lengthening traces.

(switching to prefix for easier reading) For a conjunction with 3 arguments like

(&& p q r)

p's sibling nodes are q and r, and similar for q/r. The cost of each node comes into play if we let p = (G[0,5] v0), q = v1, r = v2:

(&& (G[0,5] v0) v1 v2)

To get formal, the cost of a node is the max worst-case delay of any of its siblings, where a worst-case delay is the max time a node might have to wait to have an answer. So, p has a "worst-case delay" of 5 (might need to wait 5 time steps to know if p is true), and cost(q) = 5 and cost(r) = 5. I don't think this is a local cost function, and I think this might be difficult to extract with since nodes in the same e-class could have different worst-case delays.

And after reading up on analyses, I think egg can handle altering indices just fine.

[yihozhang]

Interesting. Is it the case that the cost of v1 can vary depending on where it occurs? So the same v1 can have multiple costs if it is used in multiple places. Do you think it makes sense to compute the cost at&& instead of at each child?

You may also be able to use more flexible cost functions by using E-class analyses. See szalinski for an example.